Commit 2025-03-30 09:34 58c274da

View on Github →

chore(Order/Interval/Set/Basic): more simp lemmas (#23435) This makes sure that Set.Ioi x can be simplified when hx : IsMax x is in context.

Estimated changes

Modified Mathlib/Combinatorics/Additive/FreimanHom.lean

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

added theorem Finset.Iio_nonempty

added theorem Finset.Ioi_nonempty

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

modified theorem Set.Iio_False

modified theorem Set.Iio_eq_empty_iff

added theorem Set.Iio_nonempty

modified theorem Set.Ioi_True

modified theorem Set.Ioi_eq_empty_iff

added theorem Set.Ioi_nonempty