Documentation

Mathlib.Topology.UnitInterval

The unit interval, as a topological space #

Use open unitInterval to turn on the notation I := Set.Icc (0 : ℝ) (1 : ℝ).

We provide basic instances, as well as a custom tactic for discharging 0 ≤ ↑x, 0 ≤ 1 - ↑x, ↑x ≤ 1, and 1 - ↑x ≤ 1 when x : I.

The unit interval #

@[reducible, inline]

The unit interval [0,1] in ℝ.

Equations
    Instances For

      The unit interval [0,1] in ℝ.

      Equations
        Instances For
          theorem unitInterval.div_mem {x y : } (hx : 0 x) (hy : 0 y) (hxy : x y) :
          @[simp]
          theorem unitInterval.coe_pos {x : unitInterval} :
          0 < x 0 < x
          @[simp]
          theorem unitInterval.coe_lt_one {x : unitInterval} :
          x < 1 x < 1

          Unit interval central symmetry.

          Equations
            Instances For

              Unit interval central symmetry.

              Equations
                Instances For
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  theorem unitInterval.coe_symm_eq (x : unitInterval) :
                  (symm x) = 1 - x
                  @[simp]
                  theorem unitInterval.symm_projIcc (x : ) :
                  symm (Set.projIcc 0 1 x) = Set.projIcc 0 1 (1 - x)
                  @[simp]
                  theorem unitInterval.symm_inj {i j : unitInterval} :
                  symm i = symm j i = j
                  theorem unitInterval.half_le_symm_iff (t : unitInterval) :
                  1 / 2 (symm t) t 1 / 2
                  @[simp]
                  theorem unitInterval.symm_eq_one {i : unitInterval} :
                  symm i = 1 i = 0
                  @[simp]
                  theorem unitInterval.symm_eq_zero {i : unitInterval} :
                  symm i = 0 i = 1
                  @[simp]
                  @[simp]
                  theorem unitInterval.symm_lt_symm {i j : unitInterval} :
                  symm i < symm j j < i
                  theorem unitInterval.nonneg (x : unitInterval) :
                  0 x
                  theorem unitInterval.le_one (x : unitInterval) :
                  x 1
                  theorem unitInterval.add_pos {t : unitInterval} {x : } (hx : 0 < x) :
                  0 < x + t
                  theorem unitInterval.nonneg' {t : unitInterval} :
                  0 t

                  like unitInterval.nonneg, but with the inequality in I.

                  theorem unitInterval.le_one' {t : unitInterval} :
                  t 1

                  like unitInterval.le_one, but with the inequality in I.

                  theorem unitInterval.eq_one_or_eq_zero_of_le_mul {i j : unitInterval} (h : i j * i) :
                  i = 0 j = 1
                  theorem unitInterval.mul_pos_mem_iff {a t : } (ha : 0 < a) :
                  a * t unitInterval t Set.Icc 0 (1 / a)

                  The unit interval as a submonoid of ℝ.

                  Equations
                    Instances For
                      theorem unitInterval.prod_mem {ι : Type u_1} {t : Finset ι} {f : ι} (h : ct, f c unitInterval) :
                      ct, f c unitInterval
                      theorem Set.abs_projIcc_sub_projIcc {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b c d : α} (h : a b) :
                      |(projIcc a b h c) - (projIcc a b h d)| |c - d|

                      Set.projIcc is a contraction.

                      def Set.Icc.addNSMul {α : Type u_1} [AddCommGroup α] [LinearOrder α] {a b : α} (h : a b) (δ : α) (n : ) :
                      (Icc a b)

                      When h : a ≤ b and δ > 0, addNSMul h δ is a sequence of points in the closed interval [a,b], which is initially equally spaced but eventually stays at the right endpoint b.

                      Equations
                        Instances For
                          theorem Set.Icc.addNSMul_zero {α : Type u_1} [AddCommGroup α] [LinearOrder α] {a b : α} (h : a b) {δ : α} :
                          (addNSMul h δ 0) = a
                          theorem Set.Icc.addNSMul_eq_right {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a b) {δ : α} [Archimedean α] ( : 0 < δ) :
                          ∃ (m : ), nm, (addNSMul h δ n) = b
                          theorem Set.Icc.monotone_addNSMul {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a b) {δ : α} ( : 0 δ) :
                          theorem Set.Icc.abs_sub_addNSMul_le {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a b) {δ : α} ( : 0 δ) {t : (Icc a b)} (n : ) (ht : t Icc (addNSMul h δ n) (addNSMul h δ (n + 1))) :
                          |t - (addNSMul h δ n)| δ
                          theorem exists_monotone_Icc_subset_open_cover_Icc {ι : Sort u_1} {a b : } (h : a b) {c : ιSet (Set.Icc a b)} (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : Set.univ ⋃ (i : ι), c i) :
                          ∃ (t : (Set.Icc a b)), (t 0) = a Monotone t (∃ (m : ), nm, (t n) = b) ∀ (n : ), ∃ (i : ι), Set.Icc (t n) (t (n + 1)) c i

                          Any open cover c of a closed interval [a, b] in ℝ can be refined to a finite partition into subintervals.

                          theorem exists_monotone_Icc_subset_open_cover_unitInterval {ι : Sort u_1} {c : ιSet unitInterval} (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : Set.univ ⋃ (i : ι), c i) :
                          ∃ (t : unitInterval), t 0 = 0 Monotone t (∃ (n : ), mn, t m = 1) ∀ (n : ), ∃ (i : ι), Set.Icc (t n) (t (n + 1)) c i

                          Any open cover of the unit interval can be refined to a finite partition into subintervals.

                          theorem exists_monotone_Icc_subset_open_cover_unitInterval_prod_self {ι : Sort u_1} {c : ιSet (unitInterval × unitInterval)} (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : Set.univ ⋃ (i : ι), c i) :
                          ∃ (t : unitInterval), t 0 = 0 Monotone t (∃ (n : ), mn, t m = 1) ∀ (n m : ), ∃ (i : ι), Set.Icc (t n) (t (n + 1)) ×ˢ Set.Icc (t m) (t (m + 1)) c i
                          @[simp]
                          theorem projIcc_eq_zero {x : } :
                          Set.projIcc 0 1 x = 0 x 0
                          @[simp]
                          theorem projIcc_eq_one {x : } :
                          Set.projIcc 0 1 x = 1 1 x

                          A tactic that solves 0 ≤ ↑x, 0 ≤ 1 - ↑x, ↑x ≤ 1, and 1 - ↑x ≤ 1 for x : I.

                          Equations
                            Instances For
                              theorem affineHomeomorph_image_I {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b : 𝕜) (h : 0 < a) :
                              (affineHomeomorph a b ) '' Set.Icc 0 1 = Set.Icc b (a + b)

                              The image of [0,1] under the homeomorphism fun x ↦ a * x + b is [b, a+b].

                              def iccHomeoI {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b : 𝕜) (h : a < b) :
                              (Set.Icc a b) ≃ₜ (Set.Icc 0 1)

                              The affine homeomorphism from a nontrivial interval [a,b] to [0,1].

                              Equations
                                Instances For
                                  @[simp]
                                  theorem iccHomeoI_apply_coe {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b : 𝕜) (h : a < b) (x : (Set.Icc a b)) :
                                  ((iccHomeoI a b h) x) = (x - a) / (b - a)
                                  @[simp]
                                  theorem iccHomeoI_symm_apply_coe {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b : 𝕜) (h : a < b) (x : (Set.Icc 0 1)) :
                                  ((iccHomeoI a b h).symm x) = (b - a) * x + a

                                  The coercion from I to ℝ≥0.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem unitInterval.coe_toNNReal (x : unitInterval) :
                                      (toNNReal x) = x