Commit 2023-01-24 12:09 a7127b7d

View on Github →

feat: port Data.Set.Intervals.Instances (#1068)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Intervals/Instances.lean

added theorem Set.Icc.coe_eq_one

added theorem Set.Icc.coe_eq_zero

added theorem Set.Icc.coe_le_one

added theorem Set.Icc.coe_mul

added theorem Set.Icc.coe_ne_one

added theorem Set.Icc.coe_ne_zero

added theorem Set.Icc.coe_nonneg

added theorem Set.Icc.coe_one

added theorem Set.Icc.coe_pow

added theorem Set.Icc.coe_zero

added theorem Set.Icc.le_one

added theorem Set.Icc.mem_iff_one_sub_mem

added theorem Set.Icc.mk_one

added theorem Set.Icc.mk_zero

added theorem Set.Icc.mul_le_left

added theorem Set.Icc.mul_le_right

added theorem Set.Icc.nonneg

added theorem Set.Icc.one_sub_le_one

added theorem Set.Icc.one_sub_mem

added theorem Set.Icc.one_sub_nonneg

added theorem Set.Ico.coe_eq_zero

added theorem Set.Ico.coe_lt_one

added theorem Set.Ico.coe_mul

added theorem Set.Ico.coe_ne_zero

added theorem Set.Ico.coe_nonneg

added theorem Set.Ico.coe_zero

added theorem Set.Ico.mk_zero

added theorem Set.Ico.nonneg

added theorem Set.Ioc.coe_eq_one

added theorem Set.Ioc.coe_le_one

added theorem Set.Ioc.coe_mul

added theorem Set.Ioc.coe_ne_one

added theorem Set.Ioc.coe_one

added theorem Set.Ioc.coe_pos

added theorem Set.Ioc.coe_pow

added theorem Set.Ioc.le_one

added theorem Set.Ioc.mk_one

added theorem Set.Ioo.coe_mul

added theorem Set.Ioo.lt_one

added theorem Set.Ioo.mem_iff_one_sub_mem

added theorem Set.Ioo.one_minus_lt_one

added theorem Set.Ioo.one_minus_pos

added theorem Set.Ioo.one_sub_mem

added theorem Set.Ioo.pos