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

        Unit interval central symmetry.

        Equations
        Instances For
          @[simp]
          @[simp]
          theorem unitInterval.symmHomeomorph_apply :
          ∀ (a : unitInterval), unitInterval.symmHomeomorph a = unitInterval.symm a

          unitInterval.symm as a Homeomorph.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            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