Commit 2026-02-23 09:20 cc17c513

View on Github →

refactor(Order/Interval/Set/LinearOrder): deprecate duplicates with stronger hypotheses (#35636) e.g. for Ioo_union_Ioi, c < b is just one of two ways you can get a c < max a b hypothesis. I kept Ico_union_Ico' and Ioc_union_Ioc' since these are more tedious to prove.

Estimated changes

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

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

modified theorem Set.Icc_union_Ici'

modified theorem Set.Ico_union_Ici'

modified theorem Set.Ico_union_Ico'

modified theorem Set.Iic_union_Icc'

modified theorem Set.Iic_union_Ioc'

modified theorem Set.Iio_union_Ico'

modified theorem Set.Iio_union_Ioo'

modified theorem Set.Ioc_union_Ioc'

modified theorem Set.Ioc_union_Ioi'

modified theorem Set.Ioo_union_Ioi'