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)` #

source

instance Set.Icc.instZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :

Zero ↑(Icc 0 1)

Equations

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

source

instance Set.Icc.instOne {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :

One ↑(Icc 0 1)

Equations

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

source

instance Set.Icc.instZeroLEOneClass {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :

ZeroLEOneClass ↑(Icc 0 1)

source

@[simp]

theorem Set.Icc.coe_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :

↑0 = 0

source

@[simp]

theorem Set.Icc.coe_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :

↑1 = 1

source

@[simp]

theorem Set.Icc.mk_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] (h : 0 ∈ Icc 0 1) :

⟨0, h⟩ = 0

source

@[simp]

theorem Set.Icc.mk_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] (h : 1 ∈ Icc 0 1) :

⟨1, h⟩ = 1

source

@[simp]

theorem Set.Icc.coe_eq_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {x : ↑(Icc 0 1)} :

↑x = 0 ↔ x = 0

source

theorem Set.Icc.coe_ne_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {x : ↑(Icc 0 1)} :

↑x ≠ 0 ↔ x ≠ 0

source

@[simp]

theorem Set.Icc.coe_eq_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {x : ↑(Icc 0 1)} :

↑x = 1 ↔ x = 1

source

theorem Set.Icc.coe_ne_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {x : ↑(Icc 0 1)} :

↑x ≠ 1 ↔ x ≠ 1

source

theorem Set.Icc.coe_nonneg {R : Type u_1} [Semiring R] [PartialOrder R] (x : ↑(Icc 0 1)) :

0 ≤ ↑x

source

theorem Set.Icc.coe_le_one {R : Type u_1} [Semiring R] [PartialOrder R] (x : ↑(Icc 0 1)) :

↑x ≤ 1

source

theorem Set.Icc.nonneg {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {t : ↑(Icc 0 1)} :

0 ≤ t

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

source

theorem Set.Icc.le_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {t : ↑(Icc 0 1)} :

t ≤ 1

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

source

instance Set.Icc.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :

Mul ↑(Icc 0 1)

Equations

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

source

instance Set.Icc.instPow {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :

Pow ↑(Icc 0 1) ℕ

Equations

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

source

@[simp]

theorem Set.Icc.coe_mul {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] (x y : ↑(Icc 0 1)) :

↑(x * y) = ↑x * ↑y

source

@[simp]

theorem Set.Icc.coe_pow {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] (x : ↑(Icc 0 1)) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

theorem Set.Icc.mul_le_left {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {x y : ↑(Icc 0 1)} :

x * y ≤ x

source

theorem Set.Icc.mul_le_right {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {x y : ↑(Icc 0 1)} :

x * y ≤ y

source

instance Set.Icc.instMonoidWithZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :

MonoidWithZero ↑(Icc 0 1)

Equations

One or more equations did not get rendered due to their size.

source

instance Set.Icc.instCommMonoidWithZero {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] :

CommMonoidWithZero ↑(Icc 0 1)

Equations

Set.Icc.instCommMonoidWithZero = { toMonoid := Set.Icc.instMonoidWithZero.toMonoid, mul_comm := ⋯, toZero := Set.Icc.instZero, zero_mul := ⋯, mul_zero := ⋯ }

source

instance Set.Icc.instCancelMonoidWithZero {R : Type u_2} [Ring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] :

CancelMonoidWithZero ↑(Icc 0 1)

Equations

Set.Icc.instCancelMonoidWithZero = { toMonoidWithZero := Set.Icc.instMonoidWithZero, toIsCancelMulZero := ⋯ }

source

instance Set.Icc.instCancelCommMonoidWithZero {R : Type u_2} [CommRing R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] :

CancelCommMonoidWithZero ↑(Icc 0 1)

Equations

Set.Icc.instCancelCommMonoidWithZero = { toCommMonoidWithZero := Set.Icc.instCommMonoidWithZero, toIsLeftCancelMulZero := ⋯ }

source

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

1 - t ∈ Icc 0 1

source

theorem Set.Icc.mem_iff_one_sub_mem {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] {t : β} :

t ∈ Icc 0 1 ↔ 1 - t ∈ Icc 0 1

source

theorem Set.Icc.one_sub_nonneg {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] (x : ↑(Icc 0 1)) :

0 ≤ 1 - ↑x

source

theorem Set.Icc.one_sub_le_one {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] (x : ↑(Icc 0 1)) :

1 - ↑x ≤ 1

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

source

instance Set.Ico.instZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] :

Zero ↑(Ico 0 1)

Equations

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

source

@[simp]

theorem Set.Ico.coe_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] :

↑0 = 0

source

@[simp]

theorem Set.Ico.mk_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] (h : 0 ∈ Ico 0 1) :

⟨0, h⟩ = 0

source

@[simp]

theorem Set.Ico.coe_eq_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] {x : ↑(Ico 0 1)} :

↑x = 0 ↔ x = 0

source

theorem Set.Ico.coe_ne_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] {x : ↑(Ico 0 1)} :

↑x ≠ 0 ↔ x ≠ 0

source

theorem Set.Ico.coe_nonneg {R : Type u_1} [Semiring R] [PartialOrder R] (x : ↑(Ico 0 1)) :

0 ≤ ↑x

source

theorem Set.Ico.coe_lt_one {R : Type u_1} [Semiring R] [PartialOrder R] (x : ↑(Ico 0 1)) :

↑x < 1

source

theorem Set.Ico.nonneg {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] {t : ↑(Ico 0 1)} :

0 ≤ t

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

source

instance Set.Ico.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :

Mul ↑(Ico 0 1)

Equations

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

source

@[simp]

theorem Set.Ico.coe_mul {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] (x y : ↑(Ico 0 1)) :

↑(x * y) = ↑x * ↑y

source

instance Set.Ico.instSemigroup {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :

Semigroup ↑(Ico 0 1)

Equations

Set.Ico.instSemigroup = { toMul := Set.Ico.instMul, mul_assoc := ⋯ }

source

instance Set.Ico.instCommSemigroup {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] :

CommSemigroup ↑(Ico 0 1)

Equations

Set.Ico.instCommSemigroup = { toSemigroup := Set.Ico.instSemigroup, mul_comm := ⋯ }

Instances for `↥(Set.Ioc 0 1)` #

source

instance Set.Ioc.instOne {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :

One ↑(Ioc 0 1)

Equations

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

source

@[simp]

theorem Set.Ioc.coe_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :

↑1 = 1

source

@[simp]

theorem Set.Ioc.mk_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (h : 1 ∈ Ioc 0 1) :

⟨1, h⟩ = 1

source

@[simp]

theorem Set.Ioc.coe_eq_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {x : ↑(Ioc 0 1)} :

↑x = 1 ↔ x = 1

source

theorem Set.Ioc.coe_ne_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {x : ↑(Ioc 0 1)} :

↑x ≠ 1 ↔ x ≠ 1

source

theorem Set.Ioc.coe_pos {R : Type u_1} [Semiring R] [PartialOrder R] (x : ↑(Ioc 0 1)) :

0 < ↑x

source

theorem Set.Ioc.coe_le_one {R : Type u_1} [Semiring R] [PartialOrder R] (x : ↑(Ioc 0 1)) :

↑x ≤ 1

source

theorem Set.Ioc.le_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {t : ↑(Ioc 0 1)} :

t ≤ 1

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

source

instance Set.Ioc.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :

Mul ↑(Ioc 0 1)

Equations

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

source

instance Set.Ioc.instPow {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :

Pow ↑(Ioc 0 1) ℕ

Equations

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

source

@[simp]

theorem Set.Ioc.coe_mul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (x y : ↑(Ioc 0 1)) :

↑(x * y) = ↑x * ↑y

source

@[simp]

theorem Set.Ioc.coe_pow {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (x : ↑(Ioc 0 1)) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

instance Set.Ioc.instSemigroup {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :

Semigroup ↑(Ioc 0 1)

Equations

Set.Ioc.instSemigroup = { toMul := Set.Ioc.instMul, mul_assoc := ⋯ }

source

instance Set.Ioc.instMonoid {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :

Monoid ↑(Ioc 0 1)

Equations

One or more equations did not get rendered due to their size.

source

instance Set.Ioc.instCommSemigroup {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :

CommSemigroup ↑(Ioc 0 1)

Equations

Set.Ioc.instCommSemigroup = { toSemigroup := Set.Ioc.instSemigroup, mul_comm := ⋯ }

source

instance Set.Ioc.instCommMonoid {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :

CommMonoid ↑(Ioc 0 1)

Equations

Set.Ioc.instCommMonoid = { toMonoid := Set.Ioc.instMonoid, mul_comm := ⋯ }

source

instance Set.Ioc.instCancelMonoid {R : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [IsDomain R] :

CancelMonoid ↑(Ioc 0 1)

Equations

Set.Ioc.instCancelMonoid = { toMonoid := Set.Ioc.instMonoid, mul_left_cancel := ⋯, mul_right_cancel := ⋯ }

source

instance Set.Ioc.instCancelCommMonoid {R : Type u_2} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [IsDomain R] :

CancelCommMonoid ↑(Ioc 0 1)

Equations

Set.Ioc.instCancelCommMonoid = { toCommMonoid := Set.Ioc.instCommMonoid, mul_left_cancel := ⋯ }

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

source

theorem Set.Ioo.pos {R : Type u_1} [Semiring R] [PartialOrder R] (x : ↑(Ioo 0 1)) :

0 < ↑x

source

theorem Set.Ioo.lt_one {R : Type u_1} [Semiring R] [PartialOrder R] (x : ↑(Ioo 0 1)) :

↑x < 1

source

instance Set.Ioo.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :

Mul ↑(Ioo 0 1)

Equations

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

source

@[simp]

theorem Set.Ioo.coe_mul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (x y : ↑(Ioo 0 1)) :

↑(x * y) = ↑x * ↑y

source

instance Set.Ioo.instSemigroup {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :

Semigroup ↑(Ioo 0 1)

Equations

Set.Ioo.instSemigroup = { toMul := Set.Ioo.instMul, mul_assoc := ⋯ }

source

instance Set.Ioo.instCommSemigroup {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :

CommSemigroup ↑(Ioo 0 1)

Equations

Set.Ioo.instCommSemigroup = { toSemigroup := Set.Ioo.instSemigroup, mul_comm := ⋯ }

source

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

1 - t ∈ Ioo 0 1

source

theorem Set.Ioo.mem_iff_one_sub_mem {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] {t : β} :

t ∈ Ioo 0 1 ↔ 1 - t ∈ Ioo 0 1

source

theorem Set.Ioo.one_minus_pos {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] (x : ↑(Ioo 0 1)) :

0 < 1 - ↑x

source

theorem Set.Ioo.one_minus_lt_one {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] (x : ↑(Ioo 0 1)) :

1 - ↑x < 1

Documentation

Mathlib.Algebra.Order.Interval.Set.Instances

Algebraic instances for unit intervals #

Main definitions #

TODO #

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

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

Instances for `↥(Set.Ioc 0 1)` #

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

Algebraic instances for unit intervals #

Main definitions #

TODO #

Instances for ↥(Set.Icc 0 1) #

Instances for ↥(Set.Ico 0 1) #

Instances for ↥(Set.Ioc 0 1) #

Instances for ↥(Set.Ioo 0 1) #

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

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

Instances for `↥(Set.Ioc 0 1)` #

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