Theorem Set.Icc.one_sub_le_one

Modification history

2026-10-07 14:19
Mathlib/Algebra/Order/Interval/Set/Instances.lean
feat(Algebra/Order/Interval/Set): generalize and add instances (#44564) …
Modified Set.Icc.one_sub_le_oneView on Github →
2023-01-24 12:09
Mathlib/Data/Set/Intervals/Instances.lean
feat: port Data.Set.Intervals.Instances (#1068)
Added Set.Icc.one_sub_le_oneView on Github →