Theorem Set.Iio_ssubset_Iio_iff

Modification history

2026-03-20 05:22
Mathlib/Order/Interval/Set/LinearOrder.lean
feat(Order/Interval/Set/Linearorder): use `to_dual` (#36821) …
Deleted Set.Iio_ssubset_Iio_iffView on Github →
2025-04-08 12:42
Mathlib/Order/Interval/Set/LinearOrder.lean
feat(Order/Interval): add strict inclusion lemmas for unbounded intervals (#23798) …
Added Set.Iio_ssubset_Iio_iffView on Github →