Commit 2026-10-07 14:19 0344eb3e

View on Github →

feat(Algebra/Order/Interval/Set): generalize and add instances (#44564) This generalizes the existing data-carrying instances on Set.Icc, Set.Ioc, Set.Ico, and Set.Ioo to more general settings, and adds new prop-valued instances.

Estimated changes

modified theorem Set.Icc.mem_iff_one_sub_mem
modified theorem Set.Icc.one_sub_le_one
modified theorem Set.Icc.one_sub_mem
modified theorem Set.Icc.one_sub_nonneg
modified theorem Set.Ico.coe_eq_zero
modified theorem Set.Ico.coe_ne_zero
modified theorem Set.Ico.coe_zero
modified theorem Set.Ico.mk_zero
modified theorem Set.Ico.nonneg
modified theorem Set.Ioo.mem_iff_one_sub_mem
modified theorem Set.Ioo.one_sub_lt_one
modified theorem Set.Ioo.one_sub_mem
modified theorem Set.Ioo.one_sub_pos