Documentation

Mathlib.Algebra.Order.Interval.Set.Instances

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:

TODO #

Instances for ↥(Set.Icc 0 1) #

source
theorem Set.Icc.coe_nonneg {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Icc 0 1)) :
0 ≤ ↑x
source
theorem Set.Icc.coe_le_one {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Icc 0 1)) :
↑x ≤ 1
source
@[instance_reducible]
instance Set.Icc.instZero {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] :
Zero ↑(Icc 0 1)
source
@[instance_reducible]
instance Set.Icc.instOne {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] :
One ↑(Icc 0 1)
source
instance Set.Icc.instZeroLEOneClass {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] :
ZeroLEOneClass ↑(Icc 0 1)
source
instance Set.Icc.instIsBotZeroClass {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] :
IsBotZeroClass ↑(Icc 0 1)
source
@[simp]
theorem Set.Icc.coe_zero {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] :
↑0 = 0
source
@[simp]
theorem Set.Icc.coe_one {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] :
↑1 = 1
source
@[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
source
@[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
source
@[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
source
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
source
@[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
source
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
source
instance Set.Icc.instNeZeroOne {R : Type u_1} [Zero R] [One R] [Preorder R] [ZeroLEOneClass R] [NeZero 1] :
NeZero 1
source
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.

source
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.

source
@[instance_reducible]
instance Set.Icc.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
Mul ↑(Icc 0 1)
source
@[instance_reducible]
instance Set.Icc.instPow {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
Pow ↑(Icc 0 1) ℕ
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
instance Set.Icc.instMulLeftMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
MulLeftMono ↑(Icc 0 1)
source
instance Set.Icc.instMulRightMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
MulRightMono ↑(Icc 0 1)
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_reducible]
instance Set.Icc.instMonoidWithZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
MonoidWithZero ↑(Icc 0 1)
source
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.

Instances For
    source
    @[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
    source
    instance Set.Icc.instIsLeftCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [IsLeftCancelMulZero R] :
    IsLeftCancelMulZero ↑(Icc 0 1)
    source
    instance Set.Icc.instIsRightCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [IsRightCancelMulZero R] :
    IsRightCancelMulZero ↑(Icc 0 1)
    source
    instance Set.Icc.instIsCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [IsCancelMulZero R] :
    IsCancelMulZero ↑(Icc 0 1)
    source
    @[instance_reducible]
    instance Set.Icc.instCommMonoidWithZero {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] :
    CommMonoidWithZero ↑(Icc 0 1)
    source
    instance Set.Icc.instIsOrderedMonoid {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] :
    IsOrderedMonoid ↑(Icc 0 1)
    source
    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
    source
    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
    source
    theorem Set.Icc.one_sub_nonneg {R : Type u_1} [AddCommGroupWithOne R] [Preorder R] [IsOrderedAddMonoid R] (x : ↑(Icc 0 1)) :
    0 ≤ 1 - ↑x
    source
    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) #

    source
    theorem Set.Ico.coe_nonneg {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ico 0 1)) :
    0 ≤ ↑x
    source
    theorem Set.Ico.coe_lt_one {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ico 0 1)) :
    ↑x < 1
    source
    @[instance_reducible]
    instance Set.Ico.instZero {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] :
    Zero ↑(Ico 0 1)
    source
    @[simp]
    theorem Set.Ico.coe_zero {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] :
    ↑0 = 0
    source
    @[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
    source
    @[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
    source
    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
    source
    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.

    source
    instance Set.Ico.instIsBotZeroClass {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] :
    IsBotZeroClass ↑(Ico 0 1)
    source
    @[instance_reducible]
    instance Set.Ico.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
    Mul ↑(Ico 0 1)
    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.instMulLeftMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
    MulLeftMono ↑(Ico 0 1)
    source
    instance Set.Ico.instMulRightMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
    MulRightMono ↑(Ico 0 1)
    source
    @[instance_reducible]
    instance Set.Ico.instSemigroup {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
    Semigroup ↑(Ico 0 1)
    source
    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.

    Instances For
      source
      @[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
      source
      @[instance_reducible]
      instance Set.Ico.instSemigroupWithZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [NeZero 1] :
      SemigroupWithZero ↑(Ico 0 1)
      source
      instance Set.Ico.instIsLeftCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [NeZero 1] [IsLeftCancelMulZero R] :
      IsLeftCancelMulZero ↑(Ico 0 1)
      source
      instance Set.Ico.instIsRightCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [NeZero 1] [IsRightCancelMulZero R] :
      IsRightCancelMulZero ↑(Ico 0 1)
      source
      instance Set.Ico.instIsCancelMulZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [NeZero 1] [IsCancelMulZero R] :
      IsCancelMulZero ↑(Ico 0 1)
      source
      @[instance_reducible]
      instance Set.Ico.instCommSemigroup {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] :
      CommSemigroup ↑(Ico 0 1)

      Instances for ↥(Set.Ioc 0 1) #

      source
      theorem Set.Ioc.coe_pos {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ioc 0 1)) :
      0 < ↑x
      source
      theorem Set.Ioc.coe_le_one {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ioc 0 1)) :
      ↑x ≤ 1
      source
      @[instance_reducible]
      instance Set.Ioc.instOne {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] :
      One ↑(Ioc 0 1)
      source
      @[simp]
      theorem Set.Ioc.coe_one {R : Type u_1} [Zero R] [One R] [PartialOrder R] [ZeroLEOneClass R] [NeZero 1] :
      ↑1 = 1
      source
      @[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
      source
      @[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
      source
      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
      source
      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.

      source
      @[instance_reducible]
      instance Set.Ioc.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
      Mul ↑(Ioc 0 1)
      source
      @[instance_reducible]
      instance Set.Ioc.instPow {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
      Pow ↑(Ioc 0 1) ℕ
      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.instMulLeftStrictMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
      MulLeftStrictMono ↑(Ioc 0 1)
      source
      instance Set.Ioc.instMulRightStrictMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
      MulRightStrictMono ↑(Ioc 0 1)
      source
      instance Set.Ioc.instMulLeftMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
      MulLeftMono ↑(Ioc 0 1)
      source
      instance Set.Ioc.instMulRightMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
      MulRightMono ↑(Ioc 0 1)
      source
      @[instance_reducible]
      instance Set.Ioc.instSemigroup {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
      Semigroup ↑(Ioc 0 1)
      source
      @[instance_reducible]
      instance Set.Ioc.instMonoid {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
      Monoid ↑(Ioc 0 1)
      source
      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.

      Instances For
        source
        @[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
        source
        instance Set.Ioc.instIsLeftCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsLeftCancelMulZero R] :
        IsLeftCancelMul ↑(Ioc 0 1)
        source
        instance Set.Ioc.instIsRightCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsRightCancelMulZero R] :
        IsRightCancelMul ↑(Ioc 0 1)
        source
        instance Set.Ioc.instIsCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsCancelMulZero R] :
        IsCancelMul ↑(Ioc 0 1)
        source
        @[instance_reducible]
        instance Set.Ioc.instCancelMonoid {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsCancelMulZero R] :
        CancelMonoid ↑(Ioc 0 1)
        source
        @[instance_reducible]
        instance Set.Ioc.instCommSemigroup {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
        CommSemigroup ↑(Ioc 0 1)
        source
        @[instance_reducible]
        instance Set.Ioc.instCommMonoid {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
        CommMonoid ↑(Ioc 0 1)
        source
        instance Set.Ioc.instIsOrderedMonoidElemOfNat {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
        IsOrderedMonoid ↑(Ioc 0 1)
        source
        @[instance_reducible]
        instance Set.Ioc.instCancelCommMonoid {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsCancelMulZero R] :
        CancelCommMonoid ↑(Ioc 0 1)

        Instances for ↥(Set.Ioo 0 1) #

        source
        theorem Set.Ioo.pos {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ioo 0 1)) :
        0 < ↑x
        source
        theorem Set.Ioo.lt_one {R : Type u_1} [Zero R] [One R] [Preorder R] (x : ↑(Ioo 0 1)) :
        ↑x < 1
        source
        @[instance_reducible]
        instance Set.Ioo.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
        Mul ↑(Ioo 0 1)
        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.instMulLeftStrictMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
        MulLeftStrictMono ↑(Ioo 0 1)
        source
        instance Set.Ioo.instMulRightStrictMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
        MulRightStrictMono ↑(Ioo 0 1)
        source
        instance Set.Ioo.instMulLeftMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
        MulLeftMono ↑(Ioo 0 1)
        source
        instance Set.Ioo.instMulRightMono {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
        MulRightMono ↑(Ioo 0 1)
        source
        @[instance_reducible]
        instance Set.Ioo.instSemigroup {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
        Semigroup ↑(Ioo 0 1)
        source
        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.

        Instances For
          source
          @[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
          source
          instance Set.Ioo.instIsLeftCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsLeftCancelMulZero R] :
          IsLeftCancelMul ↑(Ioo 0 1)
          source
          instance Set.Ioo.instIsRightCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsRightCancelMulZero R] :
          IsRightCancelMul ↑(Ioo 0 1)
          source
          instance Set.Ioo.instIsCancelMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [IsCancelMulZero R] :
          IsCancelMul ↑(Ioo 0 1)
          source
          @[instance_reducible]
          instance Set.Ioo.instCommSemigroup {R : Type u_1} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
          CommSemigroup ↑(Ioo 0 1)
          source
          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
          source
          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
          source
          theorem Set.Ioo.one_sub_pos {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [IsOrderedAddMonoid R] (x : ↑(Ioo 0 1)) :
          0 < 1 - ↑x
          source
          theorem Set.Ioo.one_sub_lt_one {R : Type u_1} [AddCommGroupWithOne R] [PartialOrder R] [IsOrderedAddMonoid R] (x : ↑(Ioo 0 1)) :
          1 - ↑x < 1
          source
          @[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.

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