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

Instances for ↥(Set.Icc 0 1) #

instance Set.Icc.instZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
Zero (Icc 0 1)
Equations
    instance Set.Icc.instOne {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
    One (Icc 0 1)
    Equations
      @[simp]
      theorem Set.Icc.coe_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
      0 = 0
      @[simp]
      theorem Set.Icc.coe_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
      1 = 1
      @[simp]
      theorem Set.Icc.mk_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] (h : 0 Icc 0 1) :
      0, h = 0
      @[simp]
      theorem Set.Icc.mk_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] (h : 1 Icc 0 1) :
      1, h = 1
      @[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
      theorem Set.Icc.coe_ne_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {x : (Icc 0 1)} :
      x 0 x 0
      @[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
      theorem Set.Icc.coe_ne_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {x : (Icc 0 1)} :
      x 1 x 1
      theorem Set.Icc.coe_nonneg {R : Type u_1} [Semiring R] [PartialOrder R] (x : (Icc 0 1)) :
      0 x
      theorem Set.Icc.coe_le_one {R : Type u_1} [Semiring R] [PartialOrder R] (x : (Icc 0 1)) :
      x 1
      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.

      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.

      instance Set.Icc.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
      Mul (Icc 0 1)
      Equations
        instance Set.Icc.instPow {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
        Pow (Icc 0 1)
        Equations
          @[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
          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
          theorem Set.Icc.one_sub_mem {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] {t : β} (ht : t Icc 0 1) :
          1 - t Icc 0 1
          theorem Set.Icc.mem_iff_one_sub_mem {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] {t : β} :
          t Icc 0 1 1 - t Icc 0 1
          theorem Set.Icc.one_sub_nonneg {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] (x : (Icc 0 1)) :
          0 1 - x
          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) #

          instance Set.Ico.instZero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] :
          Zero (Ico 0 1)
          Equations
            @[simp]
            theorem Set.Ico.coe_zero {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Nontrivial R] :
            0 = 0
            @[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
            @[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
            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
            theorem Set.Ico.coe_nonneg {R : Type u_1} [Semiring R] [PartialOrder R] (x : (Ico 0 1)) :
            0 x
            theorem Set.Ico.coe_lt_one {R : Type u_1} [Semiring R] [PartialOrder R] (x : (Ico 0 1)) :
            x < 1
            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.

            instance Set.Ico.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
            Mul (Ico 0 1)
            Equations
              @[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.instSemigroup {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] :
              Semigroup (Ico 0 1)
              Equations

                Instances for ↥(Set.Ioc 0 1) #

                instance Set.Ioc.instOne {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
                One (Ioc 0 1)
                Equations
                  @[simp]
                  theorem Set.Ioc.coe_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
                  1 = 1
                  @[simp]
                  theorem Set.Ioc.mk_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (h : 1 Ioc 0 1) :
                  1, h = 1
                  @[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
                  theorem Set.Ioc.coe_ne_one {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {x : (Ioc 0 1)} :
                  x 1 x 1
                  theorem Set.Ioc.coe_pos {R : Type u_1} [Semiring R] [PartialOrder R] (x : (Ioc 0 1)) :
                  0 < x
                  theorem Set.Ioc.coe_le_one {R : Type u_1} [Semiring R] [PartialOrder R] (x : (Ioc 0 1)) :
                  x 1
                  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.

                  instance Set.Ioc.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
                  Mul (Ioc 0 1)
                  Equations
                    instance Set.Ioc.instPow {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
                    Pow (Ioc 0 1)
                    Equations
                      @[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
                      Equations
                        instance Set.Ioc.instMonoid {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
                        Monoid (Ioc 0 1)
                        Equations

                          Instances for ↥(Set.Ioo 0 1) #

                          theorem Set.Ioo.pos {R : Type u_1} [Semiring R] [PartialOrder R] (x : (Ioo 0 1)) :
                          0 < x
                          theorem Set.Ioo.lt_one {R : Type u_1} [Semiring R] [PartialOrder R] (x : (Ioo 0 1)) :
                          x < 1
                          instance Set.Ioo.instMul {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
                          Mul (Ioo 0 1)
                          Equations
                            @[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
                            Equations
                              theorem Set.Ioo.one_sub_mem {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] {t : β} (ht : t Ioo 0 1) :
                              1 - t Ioo 0 1
                              theorem Set.Ioo.mem_iff_one_sub_mem {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] {t : β} :
                              t Ioo 0 1 1 - t Ioo 0 1
                              theorem Set.Ioo.one_minus_pos {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] (x : (Ioo 0 1)) :
                              0 < 1 - x
                              theorem Set.Ioo.one_minus_lt_one {β : Type u_2} [Ring β] [PartialOrder β] [IsOrderedRing β] (x : (Ioo 0 1)) :
                              1 - x < 1