Algebraic instances for unit intervals

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

Main definitions

The strongest typeclass provided on each interval is:

• Set.Icc.instCommMonoidWithZero, Set.Icc.instIsCancelMulZero
• Set.Ico.instCommSemigroup, Set.Ico.instSemigroupWithZero, Set.Ico.instIsCancelMulZero
• Set.Ioc.instCancelCommMonoid
• Set.Ioo.instCommSemigroup, Set.Ioo.instIsCancelMul

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)

theorem Set.Icc.coe_nonneg {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Icc 0 1)) : 0 ≤ ↑x

theorem Set.Icc.coe_le_one {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Icc 0 1)) : ↑x ≤ 1

@[instance_reducible]

instance Set.Icc.instZero {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] : Zero ↑(Icc 0 1)

Equations

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

@[instance_reducible]

instance Set.Icc.instOne {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] : One ↑(Icc 0 1)

Equations

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

instance Set.Icc.instZeroLEOneClass {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] : ZeroLEOneClass ↑(Icc 0 1)

instance Set.Icc.instIsBotZeroClass {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] : IsBotZeroClass ↑(Icc 0 1)

@[simp]

theorem Set.Icc.coe_zero {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] : ↑0 = 0

@[simp]

theorem Set.Icc.coe_one {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] : ↑1 = 1

@[simp]

theorem Set.Icc.mk_zero {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] (h : 0 ∈ Icc 0 1) : ⟨0, h⟩ = 0

@[simp]

theorem Set.Icc.mk_one {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] (h : 1 ∈ Icc 0 1) : ⟨1, h⟩ = 1

@[simp]

theorem Set.Icc.coe_eq_zero {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] {x : ↑(Icc 0 1)} : ↑x = 0 ↔ x = 0

theorem Set.Icc.coe_ne_zero {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] {x : ↑(Icc 0 1)} : ↑x ≠ 0 ↔ x ≠ 0

@[simp]

theorem Set.Icc.coe_eq_one {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] {x : ↑(Icc 0 1)} : ↑x = 1 ↔ x = 1

theorem Set.Icc.coe_ne_one {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] {x : ↑(Icc 0 1)} : ↑x ≠ 1 ↔ x ≠ 1

instance Set.Icc.instNeZeroOne {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] [NeZero 1] : NeZero 1

theorem Set.Icc.nonneg {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] {t : ↑(Icc 0 1)} : 0 ≤ t

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

theorem Set.Icc.le_one {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] {t : ↑(Icc 0 1)} : t ≤ 1

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

@[instance_reducible]

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, ⋯⟩ }

@[instance_reducible]

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, ⋯⟩ }

@[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

@[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

instance Set.Icc.instMulLeftMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] : MulLeftMono ↑(Icc 0 1)

instance Set.Icc.instMulRightMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] : MulRightMono ↑(Icc 0 1)

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

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

@[instance_reducible]

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.

def Set.Icc.coeMonoidWithZeroHom {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] : ↑(Icc 0 1) →*₀ R

The coercion from Set.Icc 0 1 as a MonoidWithZeroHom.

Equations

• Set.Icc.coeMonoidWithZeroHom = { toFun := Subtype.val, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Set.Icc.coeMonoidWithZeroHom_apply {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] (self : { x : R // x ∈ Icc 0 1 }) : coeMonoidWithZeroHom self = ↑self

instance Set.Icc.instIsLeftCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [IsLeftCancelMulZero R] : IsLeftCancelMulZero ↑(Icc 0 1)

instance Set.Icc.instIsRightCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [IsRightCancelMulZero R] : IsRightCancelMulZero ↑(Icc 0 1)

instance Set.Icc.instIsCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [IsCancelMulZero R] : IsCancelMulZero ↑(Icc 0 1)

@[instance_reducible]

instance Set.Icc.instCommMonoidWithZero {R : Type u_1} [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 := ⋯ }

instance Set.Icc.instIsOrderedMonoid {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] : IsOrderedMonoid ↑(Icc 0 1)

theorem Set.Icc.one_sub_mem {R : Type u_1} [AddCommGroupWithOne R] [Preorder R] [IsOrderedAddMonoid R] {t : R} (ht : t ∈ Icc 0 1) : 1 - t ∈ Icc 0 1

theorem Set.Icc.mem_iff_one_sub_mem {R : Type u_1} [AddCommGroupWithOne R] [Preorder R] [IsOrderedAddMonoid R] {t : R} : t ∈ Icc 0 1 ↔ 1 - t ∈ Icc 0 1

theorem Set.Icc.one_sub_nonneg {R : Type u_1} [AddCommGroupWithOne R] [Preorder R] [IsOrderedAddMonoid R] (x : ↑(Icc 0 1)) : 0 ≤ 1 - ↑x

theorem Set.Icc.one_sub_le_one {R : Type u_1} [AddCommGroupWithOne R] [Preorder R] [IsOrderedAddMonoid R] (x : ↑(Icc 0 1)) : 1 - ↑x ≤ 1

Instances for ↥(Set.Ico 0 1)

theorem Set.Ico.coe_nonneg {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ico 0 1)) : 0 ≤ ↑x

theorem Set.Ico.coe_lt_one {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ico 0 1)) : ↑x < 1

@[instance_reducible]

instance Set.Ico.instZero {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] : Zero ↑(Ico 0 1)

Equations

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

@[simp]

theorem Set.Ico.coe_zero {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] : ↑0 = 0

@[simp]

theorem Set.Ico.mk_zero {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] (h : 0 ∈ Ico 0 1) : ⟨0, h⟩ = 0

@[simp]

theorem Set.Ico.coe_eq_zero {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] {x : ↑(Ico 0 1)} : ↑x = 0 ↔ x = 0

theorem Set.Ico.coe_ne_zero {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] {x : ↑(Ico 0 1)} : ↑x ≠ 0 ↔ x ≠ 0

theorem Set.Ico.nonneg {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] {t : ↑(Ico 0 1)} : 0 ≤ t

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

instance Set.Ico.instIsBotZeroClass {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] : IsBotZeroClass ↑(Ico 0 1)

@[instance_reducible]

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, ⋯⟩ }

@[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

instance Set.Ico.instMulLeftMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] : MulLeftMono ↑(Ico 0 1)

instance Set.Ico.instMulRightMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] : MulRightMono ↑(Ico 0 1)

@[instance_reducible]

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 := ⋯ }

def Set.Ico.coeMulHom {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] : ↑(Ico 0 1) →ₙ* R

The coercion from Set.Ico 0 1 as a MulHom.

Equations

• Set.Ico.coeMulHom = { toFun := Subtype.val, map_mul' := ⋯ }

@[simp]

theorem Set.Ico.coeMulHom_apply {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] (self : { x : R // x ∈ Ico 0 1 }) : coeMulHom self = ↑self

@[instance_reducible]

instance Set.Ico.instSemigroupWithZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [NeZero 1] : SemigroupWithZero ↑(Ico 0 1)

Equations

• Set.Ico.instSemigroupWithZero = { toSemigroup := Set.Ico.instSemigroup, toZero := Set.Ico.instZero, zero_mul := ⋯, mul_zero := ⋯ }

instance Set.Ico.instIsLeftCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [NeZero 1] [IsLeftCancelMulZero R] : IsLeftCancelMulZero ↑(Ico 0 1)

instance Set.Ico.instIsRightCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [NeZero 1] [IsRightCancelMulZero R] : IsRightCancelMulZero ↑(Ico 0 1)

instance Set.Ico.instIsCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [NeZero 1] [IsCancelMulZero R] : IsCancelMulZero ↑(Ico 0 1)

@[instance_reducible]

instance Set.Ico.instCommSemigroup {R : Type u_1} [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)

theorem Set.Ioc.coe_pos {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ioc 0 1)) : 0 < ↑x

theorem Set.Ioc.coe_le_one {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ioc 0 1)) : ↑x ≤ 1

@[instance_reducible]

instance Set.Ioc.instOne {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] : One ↑(Ioc 0 1)

Equations

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

@[simp]

theorem Set.Ioc.coe_one {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] : ↑1 = 1

@[simp]

theorem Set.Ioc.mk_one {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] (h : 1 ∈ Ioc 0 1) : ⟨1, h⟩ = 1

@[simp]

theorem Set.Ioc.coe_eq_one {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] {x : ↑(Ioc 0 1)} : ↑x = 1 ↔ x = 1

theorem Set.Ioc.coe_ne_one {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] {x : ↑(Ioc 0 1)} : ↑x ≠ 1 ↔ x ≠ 1

theorem Set.Ioc.le_one {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] {t : ↑(Ioc 0 1)} : t ≤ 1

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

@[instance_reducible]

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, ⋯⟩ }

@[instance_reducible]

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, ⋯⟩ }

@[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

@[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

instance Set.Ioc.instMulLeftStrictMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : MulLeftStrictMono ↑(Ioc 0 1)

instance Set.Ioc.instMulRightStrictMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : MulRightStrictMono ↑(Ioc 0 1)

instance Set.Ioc.instMulLeftMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : MulLeftMono ↑(Ioc 0 1)

instance Set.Ioc.instMulRightMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : MulRightMono ↑(Ioc 0 1)

@[instance_reducible]

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 := ⋯ }

@[instance_reducible]

instance Set.Ioc.instMonoid {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : Monoid ↑(Ioc 0 1)

Equations

• Set.Ioc.instMonoid = { toOne := Set.Ioc.instOne, toMul := Set.Ioc.instMul, mul_assoc := ⋯, one_mul := ⋯, mul_one := ⋯, toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯ }

def Set.Ioc.coeMonoidHom {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : ↑(Ioc 0 1) →* R

The coercion from Set.Ioc 0 1 as a MonoidHom.

Equations

• Set.Ioc.coeMonoidHom = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Set.Ioc.coeMonoidHom_apply {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (self : { x : R // x ∈ Ioc 0 1 }) : coeMonoidHom self = ↑self

instance Set.Ioc.instIsLeftCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsLeftCancelMulZero R] : IsLeftCancelMul ↑(Ioc 0 1)

instance Set.Ioc.instIsRightCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsRightCancelMulZero R] : IsRightCancelMul ↑(Ioc 0 1)

instance Set.Ioc.instIsCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsCancelMulZero R] : IsCancelMul ↑(Ioc 0 1)

@[instance_reducible]

instance Set.Ioc.instCancelMonoid {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsCancelMulZero R] : CancelMonoid ↑(Ioc 0 1)

Equations

• Set.Ioc.instCancelMonoid = { toMonoid := Set.Ioc.instMonoid, toIsLeftCancelMul := ⋯, toIsRightCancelMul := ⋯ }

@[instance_reducible]

instance Set.Ioc.instCommSemigroup {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] : CommSemigroup ↑(Ioc 0 1)

Equations

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

@[instance_reducible]

instance Set.Ioc.instCommMonoid {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] : CommMonoid ↑(Ioc 0 1)

Equations

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

instance Set.Ioc.instIsOrderedMonoidElemOfNat {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] : IsOrderedMonoid ↑(Ioc 0 1)

@[instance_reducible]

instance Set.Ioc.instCancelCommMonoid {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsCancelMulZero R] : CancelCommMonoid ↑(Ioc 0 1)

Equations

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

Instances for ↥(Set.Ioo 0 1)

theorem Set.Ioo.pos {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ioo 0 1)) : 0 < ↑x

theorem Set.Ioo.lt_one {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ioo 0 1)) : ↑x < 1

@[instance_reducible]

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, ⋯⟩ }

@[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

instance Set.Ioo.instMulLeftStrictMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : MulLeftStrictMono ↑(Ioo 0 1)

instance Set.Ioo.instMulRightStrictMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : MulRightStrictMono ↑(Ioo 0 1)

instance Set.Ioo.instMulLeftMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : MulLeftMono ↑(Ioo 0 1)

instance Set.Ioo.instMulRightMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : MulRightMono ↑(Ioo 0 1)

@[instance_reducible]

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 := ⋯ }

def Set.Ioo.coeMulHom {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : ↑(Ioo 0 1) →ₙ* R

The coercion from Set.Ioo 0 1 as a MulHom.

Equations

• Set.Ioo.coeMulHom = { toFun := Subtype.val, map_mul' := ⋯ }

@[simp]

theorem Set.Ioo.coeMulHom_apply {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (self : { x : R // x ∈ Ioo 0 1 }) : coeMulHom self = ↑self

instance Set.Ioo.instIsLeftCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsLeftCancelMulZero R] : IsLeftCancelMul ↑(Ioo 0 1)

instance Set.Ioo.instIsRightCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsRightCancelMulZero R] : IsRightCancelMul ↑(Ioo 0 1)

instance Set.Ioo.instIsCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsCancelMulZero R] : IsCancelMul ↑(Ioo 0 1)

@[instance_reducible]

instance Set.Ioo.instCommSemigroup {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] : CommSemigroup ↑(Ioo 0 1)

Equations

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

theorem Set.Ioo.one_sub_mem {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [IsOrderedAddMonoid R] {t : R} (ht : t ∈ Ioo 0 1) : 1 - t ∈ Ioo 0 1

theorem Set.Ioo.mem_iff_one_sub_mem {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [IsOrderedAddMonoid R] {t : R} : t ∈ Ioo 0 1 ↔ 1 - t ∈ Ioo 0 1

theorem Set.Ioo.one_sub_pos {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [IsOrderedAddMonoid R] (x : ↑(Ioo 0 1)) : 0 < 1 - ↑x

theorem Set.Ioo.one_sub_lt_one {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [IsOrderedAddMonoid R] (x : ↑(Ioo 0 1)) : 1 - ↑x < 1

@[deprecated Set.Ioo.one_sub_pos (since := "2026-10-06")]

theorem Set.Ioo.one_minus_pos {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [IsOrderedAddMonoid R] (x : ↑(Ioo 0 1)) : 0 < 1 - ↑x

Alias of Set.Ioo.one_sub_pos.

@[deprecated Set.Ioo.one_sub_lt_one (since := "2026-10-06")]

theorem Set.Ioo.one_minus_lt_one {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [IsOrderedAddMonoid R] (x : ↑(Ioo 0 1)) : 1 - ↑x < 1

Alias of Set.Ioo.one_sub_lt_one.