Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-18 13:46 14c52e99

View on Github →

feat(data/set/intervals/instances): algebraic instances for unit intervals (#15712) Proving cancel_comm_monoid_with_zero (Icc 0 1), comm_semigroup (Ico 0 1), comm_monoid (Ioc 0 1), and comm_semigroup (Ioo 0 1) for suitably structured underlying type α.

Estimated changes

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.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.one_minus_pos
added theorem set.Ioo.one_sub_mem
added theorem set.Ioo.pos
deleted theorem unit_interval.coe_eq_one
deleted theorem unit_interval.coe_eq_zero
deleted theorem unit_interval.coe_mul
deleted theorem unit_interval.coe_one
deleted theorem unit_interval.coe_zero
deleted theorem unit_interval.mk_one
deleted theorem unit_interval.mk_zero