Theorem Finset.Iic_ssubset_Iic

Modification history

2025-04-08 12:42

Mathlib/Order/Interval/Finset/Basic.lean

feat(Order/Interval): add strict inclusion lemmas for unbounded intervals (#23798) …

Added Finset.Iic_ssubset_Iic View on Github →