# Documentation

Mathlib.Data.Set.Intervals.Instances

# Algebraic instances for unit intervals #

For suitably structured underlying type α, we exhibit the structure of the unit intervals (Set.Icc, Set.Ioc, Set.Ioc, and Set.Ioo) from 0 to 1. Note: Instances for the interval Ici 0 are dealt with in Algebra/Order/Nonneg.lean.

## Main definitions #

The strongest typeclass provided on each interval is:

• Set.Icc.cancelCommMonoidWithZero
• Set.Ico.commSemigroup
• Set.Ioc.commMonoid
• Set.Ioo.commSemigroup

## TODO #

• algebraic instances for intervals -1 to 1
• algebraic instances for Ici 1
• algebraic instances for (Ioo (-1) 1)ᶜ
• provide distribNeg instances where applicable
• prove versions of mul_le_{left,right} for other intervals
• prove versions of the lemmas in Topology/UnitInterval with ℝ generalized to some arbitrary ordered semiring

### Instances for ↥(Set.Icc 0 1)#

instance Set.Icc.zero {α : Type u_1} [inst : ] :
Zero ↑(Set.Icc 0 1)
Equations
• Set.Icc.zero = { zero := { val := 0, property := (_ : 0 Set.Icc 0 1) } }
instance Set.Icc.one {α : Type u_1} [inst : ] :
One ↑(Set.Icc 0 1)
Equations
• Set.Icc.one = { one := { val := 1, property := (_ : 1 Set.Icc 0 1) } }
@[simp]
theorem Set.Icc.coe_zero {α : Type u_1} [inst : ] :
0 = 0
@[simp]
theorem Set.Icc.coe_one {α : Type u_1} [inst : ] :
1 = 1
@[simp]
theorem Set.Icc.mk_zero {α : Type u_1} [inst : ] (h : 0 Set.Icc 0 1) :
{ val := 0, property := h } = 0
@[simp]
theorem Set.Icc.mk_one {α : Type u_1} [inst : ] (h : 1 Set.Icc 0 1) :
{ val := 1, property := h } = 1
@[simp]
theorem Set.Icc.coe_eq_zero {α : Type u_1} [inst : ] {x : ↑(Set.Icc 0 1)} :
x = 0 x = 0
theorem Set.Icc.coe_ne_zero {α : Type u_1} [inst : ] {x : ↑(Set.Icc 0 1)} :
x 0 x 0
@[simp]
theorem Set.Icc.coe_eq_one {α : Type u_1} [inst : ] {x : ↑(Set.Icc 0 1)} :
x = 1 x = 1
theorem Set.Icc.coe_ne_one {α : Type u_1} [inst : ] {x : ↑(Set.Icc 0 1)} :
x 1 x 1
theorem Set.Icc.coe_nonneg {α : Type u_1} [inst : ] (x : ↑(Set.Icc 0 1)) :
0 x
theorem Set.Icc.coe_le_one {α : Type u_1} [inst : ] (x : ↑(Set.Icc 0 1)) :
x 1
theorem Set.Icc.nonneg {α : Type u_1} [inst : ] {t : ↑(Set.Icc 0 1)} :
0 t

like coe_nonneg, but with the inequality in Icc (0:α) 1.

theorem Set.Icc.le_one {α : Type u_1} [inst : ] {t : ↑(Set.Icc 0 1)} :
t 1

like coe_le_one, but with the inequality in Icc (0:α) 1.

instance Set.Icc.mul {α : Type u_1} [inst : ] :
Mul ↑(Set.Icc 0 1)
Equations
• Set.Icc.mul = { mul := fun p q => { val := p * q, property := (_ : 0 p * q p * q 1) } }
instance Set.Icc.pow {α : Type u_1} [inst : ] :
Pow ↑(Set.Icc 0 1)
Equations
• Set.Icc.pow = { pow := fun p n => { val := p ^ n, property := (_ : 0 p ^ n p ^ n 1) } }
@[simp]
theorem Set.Icc.coe_mul {α : Type u_1} [inst : ] (x : ↑(Set.Icc 0 1)) (y : ↑(Set.Icc 0 1)) :
↑(x * y) = x * y
@[simp]
theorem Set.Icc.coe_pow {α : Type u_1} [inst : ] (x : ↑(Set.Icc 0 1)) (n : ) :
↑(x ^ n) = x ^ n
theorem Set.Icc.mul_le_left {α : Type u_1} [inst : ] {x : ↑(Set.Icc 0 1)} {y : ↑(Set.Icc 0 1)} :
x * y x
theorem Set.Icc.mul_le_right {α : Type u_1} [inst : ] {x : ↑(Set.Icc 0 1)} {y : ↑(Set.Icc 0 1)} :
x * y y
instance Set.Icc.monoidWithZero {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance Set.Icc.commMonoidWithZero {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance Set.Icc.cancelMonoidWithZero {α : Type u_1} [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance Set.Icc.cancelCommMonoidWithZero {α : Type u_1} [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
theorem Set.Icc.one_sub_mem {β : Type u_1} [inst : ] {t : β} (ht : t Set.Icc 0 1) :
1 - t Set.Icc 0 1
theorem Set.Icc.mem_iff_one_sub_mem {β : Type u_1} [inst : ] {t : β} :
t Set.Icc 0 1 1 - t Set.Icc 0 1
theorem Set.Icc.one_sub_nonneg {β : Type u_1} [inst : ] (x : ↑(Set.Icc 0 1)) :
0 1 - x
theorem Set.Icc.one_sub_le_one {β : Type u_1} [inst : ] (x : ↑(Set.Icc 0 1)) :
1 - x 1

### Instances for ↥(Set.Ico 0 1)#

instance Set.Ico.zero {α : Type u_1} [inst : ] [inst : ] :
Zero ↑(Set.Ico 0 1)
Equations
• Set.Ico.zero = { zero := { val := 0, property := (_ : 0 Set.Ico 0 1) } }
@[simp]
theorem Set.Ico.coe_zero {α : Type u_1} [inst : ] [inst : ] :
0 = 0
@[simp]
theorem Set.Ico.mk_zero {α : Type u_1} [inst : ] [inst : ] (h : 0 Set.Ico 0 1) :
{ val := 0, property := h } = 0
@[simp]
theorem Set.Ico.coe_eq_zero {α : Type u_1} [inst : ] [inst : ] {x : ↑(Set.Ico 0 1)} :
x = 0 x = 0
theorem Set.Ico.coe_ne_zero {α : Type u_1} [inst : ] [inst : ] {x : ↑(Set.Ico 0 1)} :
x 0 x 0
theorem Set.Ico.coe_nonneg {α : Type u_1} [inst : ] (x : ↑(Set.Ico 0 1)) :
0 x
theorem Set.Ico.coe_lt_one {α : Type u_1} [inst : ] (x : ↑(Set.Ico 0 1)) :
x < 1
theorem Set.Ico.nonneg {α : Type u_1} [inst : ] [inst : ] {t : ↑(Set.Ico 0 1)} :
0 t

like coe_nonneg, but with the inequality in Ico (0:α) 1.

instance Set.Ico.mul {α : Type u_1} [inst : ] :
Mul ↑(Set.Ico 0 1)
Equations
• Set.Ico.mul = { mul := fun p q => { val := p * q, property := (_ : 0 p * q p * q < 1) } }
@[simp]
theorem Set.Ico.coe_mul {α : Type u_1} [inst : ] (x : ↑(Set.Ico 0 1)) (y : ↑(Set.Ico 0 1)) :
↑(x * y) = x * y
instance Set.Ico.semigroup {α : Type u_1} [inst : ] :
Equations
instance Set.Ico.commSemigroup {α : Type u_1} [inst : ] :
Equations

### Instances for ↥(set.Ioc 0 1)#

instance Set.Ioc.one {α : Type u_1} [inst : ] [inst : ] :
One ↑(Set.Ioc 0 1)
Equations
• Set.Ioc.one = { one := { val := 1, property := (_ : 0 < 1 1 1) } }
@[simp]
theorem Set.Ioc.coe_one {α : Type u_1} [inst : ] [inst : ] :
1 = 1
@[simp]
theorem Set.Ioc.mk_one {α : Type u_1} [inst : ] [inst : ] (h : 1 Set.Ioc 0 1) :
{ val := 1, property := h } = 1
@[simp]
theorem Set.Ioc.coe_eq_one {α : Type u_1} [inst : ] [inst : ] {x : ↑(Set.Ioc 0 1)} :
x = 1 x = 1
theorem Set.Ioc.coe_ne_one {α : Type u_1} [inst : ] [inst : ] {x : ↑(Set.Ioc 0 1)} :
x 1 x 1
theorem Set.Ioc.coe_pos {α : Type u_1} [inst : ] (x : ↑(Set.Ioc 0 1)) :
0 < x
theorem Set.Ioc.coe_le_one {α : Type u_1} [inst : ] (x : ↑(Set.Ioc 0 1)) :
x 1
theorem Set.Ioc.le_one {α : Type u_1} [inst : ] [inst : ] {t : ↑(Set.Ioc 0 1)} :
t 1

like coe_le_one, but with the inequality in Ioc (0:α) 1.

instance Set.Ioc.mul {α : Type u_1} [inst : ] :
Mul ↑(Set.Ioc 0 1)
Equations
• Set.Ioc.mul = { mul := fun p q => { val := p * q, property := (_ : 0 < p * q p * q 1) } }
instance Set.Ioc.pow {α : Type u_1} [inst : ] :
Pow ↑(Set.Ioc 0 1)
Equations
• Set.Ioc.pow = { pow := fun p n => { val := p ^ n, property := (_ : 0 < p ^ n p ^ n 1) } }
@[simp]
theorem Set.Ioc.coe_mul {α : Type u_1} [inst : ] (x : ↑(Set.Ioc 0 1)) (y : ↑(Set.Ioc 0 1)) :
↑(x * y) = x * y
@[simp]
theorem Set.Ioc.coe_pow {α : Type u_1} [inst : ] (x : ↑(Set.Ioc 0 1)) (n : ) :
↑(x ^ n) = x ^ n
instance Set.Ioc.semigroup {α : Type u_1} [inst : ] :
Equations
instance Set.Ioc.monoid {α : Type u_1} [inst : ] [inst : ] :
Monoid ↑(Set.Ioc 0 1)
Equations
• One or more equations did not get rendered due to their size.
instance Set.Ioc.commSemigroup {α : Type u_1} [inst : ] :
Equations
instance Set.Ioc.commMonoid {α : Type u_1} [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance Set.Ioc.cancelMonoid {α : Type u_1} [inst : ] [inst : ] :
Equations
instance Set.Ioc.cancelCommMonoid {α : Type u_1} [inst : ] [inst : ] :
Equations
• Set.Ioc.cancelCommMonoid = let src := Set.Ioc.cancelMonoid; let src_1 := Set.Ioc.commMonoid; CancelCommMonoid.mk (_ : ∀ (a b : ↑(Set.Ioc 0 1)), a * b = b * a)

### Instances for ↥(Set.Ioo 0 1)#

theorem Set.Ioo.pos {α : Type u_1} [inst : ] (x : ↑(Set.Ioo 0 1)) :
0 < x
theorem Set.Ioo.lt_one {α : Type u_1} [inst : ] (x : ↑(Set.Ioo 0 1)) :
x < 1
instance Set.Ioo.mul {α : Type u_1} [inst : ] :
Mul ↑(Set.Ioo 0 1)
Equations
• Set.Ioo.mul = { mul := fun p q => { val := p * q, property := (_ : 0 < p * q p * q < 1) } }
@[simp]
theorem Set.Ioo.coe_mul {α : Type u_1} [inst : ] (x : ↑(Set.Ioo 0 1)) (y : ↑(Set.Ioo 0 1)) :
↑(x * y) = x * y
instance Set.Ioo.semigroup {α : Type u_1} [inst : ] :
Equations
instance Set.Ioo.commSemigroup {α : Type u_1} [inst : ] :
Equations
theorem Set.Ioo.one_sub_mem {β : Type u_1} [inst : ] {t : β} (ht : t Set.Ioo 0 1) :
1 - t Set.Ioo 0 1
theorem Set.Ioo.mem_iff_one_sub_mem {β : Type u_1} [inst : ] {t : β} :
t Set.Ioo 0 1 1 - t Set.Ioo 0 1
theorem Set.Ioo.one_minus_pos {β : Type u_1} [inst : ] (x : ↑(Set.Ioo 0 1)) :
0 < 1 - x
theorem Set.Ioo.one_minus_lt_one {β : Type u_1} [inst : ] (x : ↑(Set.Ioo 0 1)) :
1 - x < 1