Commit 2026-07-01 06:16 f9c3ad4d

View on Github →

feat(Order): Ici (1 : α) = univ when IsBotOneClass α (#40762) From PFR

Estimated changes

Modified Mathlib/Algebra/Order/Group/Pointwise/Interval.lean

deleted theorem Set.Ici_one_eq_univ

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

modified theorem MeasureTheory.Measure.mkMetric_mono

modified theorem MeasureTheory.OuterMeasure.mkMetric_mono

Modified Mathlib/Order/Interval/Finset/Defs.lean

added theorem Finset.Ici_one_eq_univ

Modified Mathlib/Order/Interval/Set/Basic.lean

added theorem Set.Ici_one_eq_univ