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:

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

ink

instance Set.Icc.zero {α : Type u_1} [inst : OrderedSemiring α] :

Zero ↑(Set.Icc 0 1)

Equations

Set.Icc.zero = { zero := { val := 0, property := (_ : 0 ∈ Set.Icc 0 1) } }

source

ink

instance Set.Icc.one {α : Type u_1} [inst : OrderedSemiring α] :

One ↑(Set.Icc 0 1)

Equations

Set.Icc.one = { one := { val := 1, property := (_ : 1 ∈ Set.Icc 0 1) } }

source

ink

@[simp]

theorem Set.Icc.coe_zero {α : Type u_1} [inst : OrderedSemiring α] :

↑0 = 0

source

ink

@[simp]

theorem Set.Icc.coe_one {α : Type u_1} [inst : OrderedSemiring α] :

↑1 = 1

source

ink

@[simp]

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

{ val := 0, property := h } = 0

source

ink

@[simp]

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

{ val := 1, property := h } = 1

source

ink

@[simp]

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

↑x = 0 ↔ x = 0

source

ink

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

↑x ≠ 0 ↔ x ≠ 0

source

ink

@[simp]

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

↑x = 1 ↔ x = 1

source

ink

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

↑x ≠ 1 ↔ x ≠ 1

source

ink

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

0 ≤ ↑x

source

ink

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

↑x ≤ 1

source

ink

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

0 ≤ t

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

source

ink

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

t ≤ 1

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

source

ink

instance Set.Icc.mul {α : Type u_1} [inst : OrderedSemiring α] :

Mul ↑(Set.Icc 0 1)

Equations

Set.Icc.mul = { mul := fun p q => { val := ↑p * ↑q, property := (_ : 0 ≤ ↑p * ↑q ∧ ↑p * ↑q ≤ 1) } }

source

ink

instance Set.Icc.pow {α : Type u_1} [inst : OrderedSemiring α] :

Pow ↑(Set.Icc 0 1) ℕ

Equations

Set.Icc.pow = { pow := fun p n => { val := ↑p ^ n, property := (_ : 0 ≤ ↑p ^ n ∧ ↑p ^ n ≤ 1) } }

source

ink

@[simp]

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

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

source

ink

@[simp]

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

↑(x ^ n) = ↑x ^ n

source

ink

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

x * y ≤ x

source

ink

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

x * y ≤ y

source

ink

instance Set.Icc.monoidWithZero {α : Type u_1} [inst : OrderedSemiring α] :

MonoidWithZero ↑(Set.Icc 0 1)

Equations

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

source

ink

instance Set.Icc.commMonoidWithZero {α : Type u_1} [inst : OrderedCommSemiring α] :

CommMonoidWithZero ↑(Set.Icc 0 1)

Equations

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

source

ink

instance Set.Icc.cancelMonoidWithZero {α : Type u_1} [inst : OrderedRing α] [inst : NoZeroDivisors α] :

CancelMonoidWithZero ↑(Set.Icc 0 1)

Equations

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

source

ink

instance Set.Icc.cancelCommMonoidWithZero {α : Type u_1} [inst : OrderedCommRing α] [inst : NoZeroDivisors α] :

CancelCommMonoidWithZero ↑(Set.Icc 0 1)

Equations

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

source

ink

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

1 - t ∈ Set.Icc 0 1

source

ink

theorem Set.Icc.mem_iff_one_sub_mem {β : Type u_1} [inst : OrderedRing β] {t : β} :

t ∈ Set.Icc 0 1 ↔ 1 - t ∈ Set.Icc 0 1

source

ink

theorem Set.Icc.one_sub_nonneg {β : Type u_1} [inst : OrderedRing β] (x : ↑(Set.Icc 0 1)) :

0 ≤ 1 - ↑x

source

ink

theorem Set.Icc.one_sub_le_one {β : Type u_1} [inst : OrderedRing β] (x : ↑(Set.Icc 0 1)) :

1 - ↑x ≤ 1

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

source

ink

instance Set.Ico.zero {α : Type u_1} [inst : OrderedSemiring α] [inst : Nontrivial α] :

Zero ↑(Set.Ico 0 1)

Equations

Set.Ico.zero = { zero := { val := 0, property := (_ : 0 ∈ Set.Ico 0 1) } }

source

ink

@[simp]

theorem Set.Ico.coe_zero {α : Type u_1} [inst : OrderedSemiring α] [inst : Nontrivial α] :

↑0 = 0

source

ink

@[simp]

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

{ val := 0, property := h } = 0

source

ink

@[simp]

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

↑x = 0 ↔ x = 0

source

ink

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

↑x ≠ 0 ↔ x ≠ 0

source

ink

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

0 ≤ ↑x

source

ink

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

↑x < 1

source

ink

theorem Set.Ico.nonneg {α : Type u_1} [inst : OrderedSemiring α] [inst : Nontrivial α] {t : ↑(Set.Ico 0 1)} :

0 ≤ t

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

source

ink

instance Set.Ico.mul {α : Type u_1} [inst : OrderedSemiring α] :

Mul ↑(Set.Ico 0 1)

Equations

Set.Ico.mul = { mul := fun p q => { val := ↑p * ↑q, property := (_ : 0 ≤ ↑p * ↑q ∧ ↑p * ↑q < 1) } }

source

ink

@[simp]

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

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

source

ink

instance Set.Ico.semigroup {α : Type u_1} [inst : OrderedSemiring α] :

Semigroup ↑(Set.Ico 0 1)

Equations

Set.Ico.semigroup = Function.Injective.semigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ico 0 1)), ↑(x * y) = ↑x * ↑y)

source

ink

instance Set.Ico.commSemigroup {α : Type u_1} [inst : OrderedCommSemiring α] :

CommSemigroup ↑(Set.Ico 0 1)

Equations

Set.Ico.commSemigroup = Function.Injective.commSemigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ico 0 1)), ↑(x * y) = ↑x * ↑y)

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

source

ink

instance Set.Ioc.one {α : Type u_1} [inst : StrictOrderedSemiring α] [inst : Nontrivial α] :

One ↑(Set.Ioc 0 1)

Equations

Set.Ioc.one = { one := { val := 1, property := (_ : 0 < 1 ∧ 1 ≤ 1) } }

source

ink

@[simp]

theorem Set.Ioc.coe_one {α : Type u_1} [inst : StrictOrderedSemiring α] [inst : Nontrivial α] :

↑1 = 1

source

ink

@[simp]

theorem Set.Ioc.mk_one {α : Type u_1} [inst : StrictOrderedSemiring α] [inst : Nontrivial α] (h : 1 ∈ Set.Ioc 0 1) :

{ val := 1, property := h } = 1

source

ink

@[simp]

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

↑x = 1 ↔ x = 1

source

ink

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

↑x ≠ 1 ↔ x ≠ 1

source

ink

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

0 < ↑x

source

ink

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

↑x ≤ 1

source

ink

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

t ≤ 1

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

source

ink

instance Set.Ioc.mul {α : Type u_1} [inst : StrictOrderedSemiring α] :

Mul ↑(Set.Ioc 0 1)

Equations

Set.Ioc.mul = { mul := fun p q => { val := ↑p * ↑q, property := (_ : 0 < ↑p * ↑q ∧ ↑p * ↑q ≤ 1) } }

source

ink

instance Set.Ioc.pow {α : Type u_1} [inst : StrictOrderedSemiring α] :

Pow ↑(Set.Ioc 0 1) ℕ

Equations

Set.Ioc.pow = { pow := fun p n => { val := ↑p ^ n, property := (_ : 0 < ↑p ^ n ∧ ↑p ^ n ≤ 1) } }

source

ink

@[simp]

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

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

source

ink

@[simp]

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

↑(x ^ n) = ↑x ^ n

source

ink

instance Set.Ioc.semigroup {α : Type u_1} [inst : StrictOrderedSemiring α] :

Semigroup ↑(Set.Ioc 0 1)

Equations

Set.Ioc.semigroup = Function.Injective.semigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ioc 0 1)), ↑(x * y) = ↑x * ↑y)

source

ink

instance Set.Ioc.monoid {α : Type u_1} [inst : StrictOrderedSemiring α] [inst : Nontrivial α] :

Monoid ↑(Set.Ioc 0 1)

Equations

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

source

ink

instance Set.Ioc.commSemigroup {α : Type u_1} [inst : StrictOrderedCommSemiring α] :

CommSemigroup ↑(Set.Ioc 0 1)

Equations

Set.Ioc.commSemigroup = Function.Injective.commSemigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ioc 0 1)), ↑(x * y) = ↑x * ↑y)

source

ink

instance Set.Ioc.commMonoid {α : Type u_1} [inst : StrictOrderedCommSemiring α] [inst : Nontrivial α] :

CommMonoid ↑(Set.Ioc 0 1)

Equations

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

source

ink

instance Set.Ioc.cancelMonoid {α : Type u_1} [inst : StrictOrderedRing α] [inst : IsDomain α] :

CancelMonoid ↑(Set.Ioc 0 1)

Equations

Set.Ioc.cancelMonoid = let src := Set.Ioc.monoid; CancelMonoid.mk (_ : ∀ (x b x_1 : ↑(Set.Ioc 0 1)), x * b = x_1 * b → x = x_1)

source

ink

instance Set.Ioc.cancelCommMonoid {α : Type u_1} [inst : StrictOrderedCommRing α] [inst : IsDomain α] :

CancelCommMonoid ↑(Set.Ioc 0 1)

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

source

ink

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

0 < ↑x

source

ink

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

↑x < 1

source

ink

instance Set.Ioo.mul {α : Type u_1} [inst : StrictOrderedSemiring α] :

Mul ↑(Set.Ioo 0 1)

Equations

Set.Ioo.mul = { mul := fun p q => { val := ↑p * ↑q, property := (_ : 0 < ↑p * ↑q ∧ ↑p * ↑q < 1) } }

source

ink

@[simp]

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

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

source

ink

instance Set.Ioo.semigroup {α : Type u_1} [inst : StrictOrderedSemiring α] :

Semigroup ↑(Set.Ioo 0 1)

Equations

Set.Ioo.semigroup = Function.Injective.semigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ioo 0 1)), ↑(x * y) = ↑x * ↑y)

source

ink

instance Set.Ioo.commSemigroup {α : Type u_1} [inst : StrictOrderedCommSemiring α] :

CommSemigroup ↑(Set.Ioo 0 1)

Equations

Set.Ioo.commSemigroup = Function.Injective.commSemigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ioo 0 1)), ↑(x * y) = ↑x * ↑y)