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
    theorem unitInterval.mul_mem {x : } {y : } (hx : x unitInterval) (hy : y unitInterval) :
    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
    Equations

    Unit interval central symmetry.

    Equations
    Instances For
      @[simp]

      unitInterval.symm as a Homeomorph.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem unitInterval.symmHomeomorph_apply :
        ∀ (a : unitInterval), unitInterval.symmHomeomorph a = unitInterval.symm a
        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 : unitInterval} {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)
        Equations
        • One or more equations did not get rendered due to their size.
        theorem Set.abs_projIcc_sub_projIcc {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} {d : α} (h : a b) :
        |(Set.projIcc a b h c) - (Set.projIcc a b h d)| |c - d|

        Set.projIcc is a contraction.

        def Set.Icc.addNSMul {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} (h : a b) (δ : α) (n : ) :
        (Set.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} [LinearOrderedAddCommGroup α] {a : α} {b : α} (h : a b) {δ : α} :
          (Set.Icc.addNSMul h δ 0) = a
          theorem Set.Icc.addNSMul_eq_right {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} (h : a b) {δ : α} [Archimedean α] (hδ : 0 < δ) :
          ∃ (m : ), nm, (Set.Icc.addNSMul h δ n) = b
          theorem Set.Icc.monotone_addNSMul {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} (h : a b) {δ : α} (hδ : 0 δ) :
          theorem Set.Icc.abs_sub_addNSMul_le {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} (h : a b) {δ : α} (hδ : 0 δ) {t : (Set.Icc a b)} (n : ) (ht : t Set.Icc (Set.Icc.addNSMul h δ n) (Set.Icc.addNSMul h δ (n + 1))) :
          |t - (Set.Icc.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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] (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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] (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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] (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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] (a : 𝕜) (b : 𝕜) (h : a < b) (x : (Set.Icc 0 1)) :
              ((iccHomeoI a b h).symm x) = (b - a) * x + a