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} [OrderedSemiring α] : Zero ↑(Set.Icc 0 1)

Equations

• Set.Icc.zero = { zero := ⟨0, ⋯⟩ }

instance Set.Icc.one {α : Type u_1} [OrderedSemiring α] : One ↑(Set.Icc 0 1)

Equations

• Set.Icc.one = { one := ⟨1, ⋯⟩ }

@[simp]

theorem Set.Icc.coe_zero {α : Type u_1} [OrderedSemiring α] : ↑0 = 0

@[simp]

theorem Set.Icc.coe_one {α : Type u_1} [OrderedSemiring α] : ↑1 = 1

@[simp]

theorem Set.Icc.mk_zero {α : Type u_1} [OrderedSemiring α] (h : 0 ∈ Set.Icc 0 1) : ⟨0, h⟩ = 0

@[simp]

theorem Set.Icc.mk_one {α : Type u_1} [OrderedSemiring α] (h : 1 ∈ Set.Icc 0 1) : ⟨1, h⟩ = 1

@[simp]

theorem Set.Icc.coe_eq_zero {α : Type u_1} [OrderedSemiring α] {x : ↑(Set.Icc 0 1)} : ↑x = 0 ↔ x = 0

theorem Set.Icc.coe_ne_zero {α : Type u_1} [OrderedSemiring α] {x : ↑(Set.Icc 0 1)} : ↑x ≠ 0 ↔ x ≠ 0

@[simp]

theorem Set.Icc.coe_eq_one {α : Type u_1} [OrderedSemiring α] {x : ↑(Set.Icc 0 1)} : ↑x = 1 ↔ x = 1

theorem Set.Icc.coe_ne_one {α : Type u_1} [OrderedSemiring α] {x : ↑(Set.Icc 0 1)} : ↑x ≠ 1 ↔ x ≠ 1

theorem Set.Icc.coe_nonneg {α : Type u_1} [OrderedSemiring α] (x : ↑(Set.Icc 0 1)) : 0 ≤ ↑x

theorem Set.Icc.coe_le_one {α : Type u_1} [OrderedSemiring α] (x : ↑(Set.Icc 0 1)) : ↑x ≤ 1

theorem Set.Icc.nonneg {α : Type u_1} [OrderedSemiring α] {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} [OrderedSemiring α] {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} [OrderedSemiring α] : Mul ↑(Set.Icc 0 1)

Equations

• Set.Icc.mul = { mul := fun (p q : ↑(Set.Icc 0 1)) => ⟨↑p * ↑q, ⋯⟩ }

instance Set.Icc.pow {α : Type u_1} [OrderedSemiring α] : Pow ↑(Set.Icc 0 1) ℕ

Equations

• Set.Icc.pow = { pow := fun (p : ↑(Set.Icc 0 1)) (n : ℕ) => ⟨↑p ^ n, ⋯⟩ }

@[simp]

theorem Set.Icc.coe_mul {α : Type u_1} [OrderedSemiring α] (x : ↑(Set.Icc 0 1)) (y : ↑(Set.Icc 0 1)) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem Set.Icc.coe_pow {α : Type u_1} [OrderedSemiring α] (x : ↑(Set.Icc 0 1)) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

theorem Set.Icc.mul_le_left {α : Type u_1} [OrderedSemiring α] {x : ↑(Set.Icc 0 1)} {y : ↑(Set.Icc 0 1)} : x * y ≤ x

theorem Set.Icc.mul_le_right {α : Type u_1} [OrderedSemiring α] {x : ↑(Set.Icc 0 1)} {y : ↑(Set.Icc 0 1)} : x * y ≤ y

instance Set.Icc.monoidWithZero {α : Type u_1} [OrderedSemiring α] : MonoidWithZero ↑(Set.Icc 0 1)

Equations

• Set.Icc.monoidWithZero = Function.Injective.monoidWithZero (fun (a : { x : α // x ∈ Set.Icc 0 1 }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯

instance Set.Icc.commMonoidWithZero {α : Type u_2} [OrderedCommSemiring α] : CommMonoidWithZero ↑(Set.Icc 0 1)

Equations

• Set.Icc.commMonoidWithZero = Function.Injective.commMonoidWithZero (fun (a : { x : α // x ∈ Set.Icc 0 1 }) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯

instance Set.Icc.cancelMonoidWithZero {α : Type u_2} [OrderedRing α] [NoZeroDivisors α] : CancelMonoidWithZero ↑(Set.Icc 0 1)

Equations

• Set.Icc.cancelMonoidWithZero = Function.Injective.cancelMonoidWithZero (fun (v : ↑(Set.Icc 0 1)) => ↑v) ⋯ ⋯ ⋯ ⋯ ⋯

instance Set.Icc.cancelCommMonoidWithZero {α : Type u_2} [OrderedCommRing α] [NoZeroDivisors α] : CancelCommMonoidWithZero ↑(Set.Icc 0 1)

Equations

• Set.Icc.cancelCommMonoidWithZero = Function.Injective.cancelCommMonoidWithZero (fun (v : ↑(Set.Icc 0 1)) => ↑v) ⋯ ⋯ ⋯ ⋯ ⋯

theorem Set.Icc.one_sub_mem {β : Type u_2} [OrderedRing β] {t : β} (ht : t ∈ Set.Icc 0 1) : 1 - t ∈ Set.Icc 0 1

theorem Set.Icc.mem_iff_one_sub_mem {β : Type u_2} [OrderedRing β] {t : β} : t ∈ Set.Icc 0 1 ↔ 1 - t ∈ Set.Icc 0 1

theorem Set.Icc.one_sub_nonneg {β : Type u_2} [OrderedRing β] (x : ↑(Set.Icc 0 1)) : 0 ≤ 1 - ↑x

theorem Set.Icc.one_sub_le_one {β : Type u_2} [OrderedRing β] (x : ↑(Set.Icc 0 1)) : 1 - ↑x ≤ 1

Instances for ↥(Set.Ico 0 1)

instance Set.Ico.zero {α : Type u_1} [OrderedSemiring α] [Nontrivial α] : Zero ↑(Set.Ico 0 1)

Equations

• Set.Ico.zero = { zero := ⟨0, ⋯⟩ }

@[simp]

theorem Set.Ico.coe_zero {α : Type u_1} [OrderedSemiring α] [Nontrivial α] : ↑0 = 0

@[simp]

theorem Set.Ico.mk_zero {α : Type u_1} [OrderedSemiring α] [Nontrivial α] (h : 0 ∈ Set.Ico 0 1) : ⟨0, h⟩ = 0

@[simp]

theorem Set.Ico.coe_eq_zero {α : Type u_1} [OrderedSemiring α] [Nontrivial α] {x : ↑(Set.Ico 0 1)} : ↑x = 0 ↔ x = 0

theorem Set.Ico.coe_ne_zero {α : Type u_1} [OrderedSemiring α] [Nontrivial α] {x : ↑(Set.Ico 0 1)} : ↑x ≠ 0 ↔ x ≠ 0

theorem Set.Ico.coe_nonneg {α : Type u_1} [OrderedSemiring α] (x : ↑(Set.Ico 0 1)) : 0 ≤ ↑x

theorem Set.Ico.coe_lt_one {α : Type u_1} [OrderedSemiring α] (x : ↑(Set.Ico 0 1)) : ↑x < 1

theorem Set.Ico.nonneg {α : Type u_1} [OrderedSemiring α] [Nontrivial α] {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} [OrderedSemiring α] : Mul ↑(Set.Ico 0 1)

Equations

• Set.Ico.mul = { mul := fun (p q : ↑(Set.Ico 0 1)) => ⟨↑p * ↑q, ⋯⟩ }

@[simp]

theorem Set.Ico.coe_mul {α : Type u_1} [OrderedSemiring α] (x : ↑(Set.Ico 0 1)) (y : ↑(Set.Ico 0 1)) : ↑(x * y) = ↑x * ↑y

instance Set.Ico.semigroup {α : Type u_1} [OrderedSemiring α] : Semigroup ↑(Set.Ico 0 1)

Equations

• Set.Ico.semigroup = Function.Injective.semigroup (fun (a : { x : α // x ∈ Set.Ico 0 1 }) => ↑a) ⋯ ⋯

instance Set.Ico.commSemigroup {α : Type u_2} [OrderedCommSemiring α] : CommSemigroup ↑(Set.Ico 0 1)

Equations

• Set.Ico.commSemigroup = Function.Injective.commSemigroup (fun (a : { x : α // x ∈ Set.Ico 0 1 }) => ↑a) ⋯ ⋯

Instances for ↥(Set.Ioc 0 1)

instance Set.Ioc.one {α : Type u_1} [StrictOrderedSemiring α] : One ↑(Set.Ioc 0 1)

Equations

• Set.Ioc.one = { one := ⟨1, ⋯⟩ }

@[simp]

theorem Set.Ioc.coe_one {α : Type u_1} [StrictOrderedSemiring α] : ↑1 = 1

@[simp]

theorem Set.Ioc.mk_one {α : Type u_1} [StrictOrderedSemiring α] (h : 1 ∈ Set.Ioc 0 1) : ⟨1, h⟩ = 1

@[simp]

theorem Set.Ioc.coe_eq_one {α : Type u_1} [StrictOrderedSemiring α] {x : ↑(Set.Ioc 0 1)} : ↑x = 1 ↔ x = 1

theorem Set.Ioc.coe_ne_one {α : Type u_1} [StrictOrderedSemiring α] {x : ↑(Set.Ioc 0 1)} : ↑x ≠ 1 ↔ x ≠ 1

theorem Set.Ioc.coe_pos {α : Type u_1} [StrictOrderedSemiring α] (x : ↑(Set.Ioc 0 1)) : 0 < ↑x

theorem Set.Ioc.coe_le_one {α : Type u_1} [StrictOrderedSemiring α] (x : ↑(Set.Ioc 0 1)) : ↑x ≤ 1

theorem Set.Ioc.le_one {α : Type u_1} [StrictOrderedSemiring α] {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} [StrictOrderedSemiring α] : Mul ↑(Set.Ioc 0 1)

Equations

• Set.Ioc.mul = { mul := fun (p q : ↑(Set.Ioc 0 1)) => ⟨↑p * ↑q, ⋯⟩ }

instance Set.Ioc.pow {α : Type u_1} [StrictOrderedSemiring α] : Pow ↑(Set.Ioc 0 1) ℕ

Equations

• Set.Ioc.pow = { pow := fun (p : ↑(Set.Ioc 0 1)) (n : ℕ) => ⟨↑p ^ n, ⋯⟩ }

@[simp]

theorem Set.Ioc.coe_mul {α : Type u_1} [StrictOrderedSemiring α] (x : ↑(Set.Ioc 0 1)) (y : ↑(Set.Ioc 0 1)) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem Set.Ioc.coe_pow {α : Type u_1} [StrictOrderedSemiring α] (x : ↑(Set.Ioc 0 1)) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

instance Set.Ioc.semigroup {α : Type u_1} [StrictOrderedSemiring α] : Semigroup ↑(Set.Ioc 0 1)

Equations

• Set.Ioc.semigroup = Function.Injective.semigroup (fun (a : { x : α // x ∈ Set.Ioc 0 1 }) => ↑a) ⋯ ⋯

instance Set.Ioc.monoid {α : Type u_1} [StrictOrderedSemiring α] : Monoid ↑(Set.Ioc 0 1)

Equations

• Set.Ioc.monoid = Function.Injective.monoid (fun (a : { x : α // x ∈ Set.Ioc 0 1 }) => ↑a) ⋯ ⋯ ⋯ ⋯

instance Set.Ioc.commSemigroup {α : Type u_2} [StrictOrderedCommSemiring α] : CommSemigroup ↑(Set.Ioc 0 1)

Equations

• Set.Ioc.commSemigroup = Function.Injective.commSemigroup (fun (a : { x : α // x ∈ Set.Ioc 0 1 }) => ↑a) ⋯ ⋯

instance Set.Ioc.commMonoid {α : Type u_2} [StrictOrderedCommSemiring α] : CommMonoid ↑(Set.Ioc 0 1)

Equations

• Set.Ioc.commMonoid = Function.Injective.commMonoid (fun (a : { x : α // x ∈ Set.Ioc 0 1 }) => ↑a) ⋯ ⋯ ⋯ ⋯

instance Set.Ioc.cancelMonoid {α : Type u_2} [StrictOrderedRing α] [IsDomain α] : CancelMonoid ↑(Set.Ioc 0 1)

Equations

• Set.Ioc.cancelMonoid = CancelMonoid.mk ⋯

instance Set.Ioc.cancelCommMonoid {α : Type u_2} [StrictOrderedCommRing α] [IsDomain α] : CancelCommMonoid ↑(Set.Ioc 0 1)

Equations

• Set.Ioc.cancelCommMonoid = CancelCommMonoid.mk ⋯

Instances for ↥(Set.Ioo 0 1)

theorem Set.Ioo.pos {α : Type u_1} [StrictOrderedSemiring α] (x : ↑(Set.Ioo 0 1)) : 0 < ↑x

theorem Set.Ioo.lt_one {α : Type u_1} [StrictOrderedSemiring α] (x : ↑(Set.Ioo 0 1)) : ↑x < 1

instance Set.Ioo.mul {α : Type u_1} [StrictOrderedSemiring α] : Mul ↑(Set.Ioo 0 1)

Equations

• Set.Ioo.mul = { mul := fun (p q : ↑(Set.Ioo 0 1)) => ⟨↑p * ↑q, ⋯⟩ }

@[simp]

theorem Set.Ioo.coe_mul {α : Type u_1} [StrictOrderedSemiring α] (x : ↑(Set.Ioo 0 1)) (y : ↑(Set.Ioo 0 1)) : ↑(x * y) = ↑x * ↑y

instance Set.Ioo.semigroup {α : Type u_1} [StrictOrderedSemiring α] : Semigroup ↑(Set.Ioo 0 1)

Equations

• Set.Ioo.semigroup = Function.Injective.semigroup (fun (a : { x : α // x ∈ Set.Ioo 0 1 }) => ↑a) ⋯ ⋯

instance Set.Ioo.commSemigroup {α : Type u_2} [StrictOrderedCommSemiring α] : CommSemigroup ↑(Set.Ioo 0 1)

Equations

• Set.Ioo.commSemigroup = Function.Injective.commSemigroup (fun (a : { x : α // x ∈ Set.Ioo 0 1 }) => ↑a) ⋯ ⋯

theorem Set.Ioo.one_sub_mem {β : Type u_2} [OrderedRing β] {t : β} (ht : t ∈ Set.Ioo 0 1) : 1 - t ∈ Set.Ioo 0 1

theorem Set.Ioo.mem_iff_one_sub_mem {β : Type u_2} [OrderedRing β] {t : β} : t ∈ Set.Ioo 0 1 ↔ 1 - t ∈ Set.Ioo 0 1

theorem Set.Ioo.one_minus_pos {β : Type u_2} [OrderedRing β] (x : ↑(Set.Ioo 0 1)) : 0 < 1 - ↑x

theorem Set.Ioo.one_minus_lt_one {β : Type u_2} [OrderedRing β] (x : ↑(Set.Ioo 0 1)) : 1 - ↑x < 1