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

The unit interval [0,1] in ℝ.

Equations
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

Unit interval central symmetry.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
theorem unitInterval.coe_symm_eq (x : unitInterval) :
(symm x) = 1 - x

unitInterval.symm as a Homeomorph.

Equations
  • One or more equations did not get rendered due to their size.
@[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
theorem unitInterval.prod_mem {ι : Type u_1} {t : Finset ι} {f : ι} (h : ct, f c unitInterval) :
ct, f c unitInterval
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) :
|(projIcc a b h c) - (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 : ) :
(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
theorem Set.Icc.addNSMul_zero {α : Type u_1} [LinearOrderedAddCommGroup α] {a b : α} (h : a b) {δ : α} :
(addNSMul h δ 0) = a
theorem Set.Icc.addNSMul_eq_right {α : Type u_1} [LinearOrderedAddCommGroup α] {a b : α} (h : a b) {δ : α} [Archimedean α] (hδ : 0 < δ) :
∃ (m : ), nm, (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 : (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
theorem affineHomeomorph_image_I {𝕜 : Type u_1} [LinearOrderedField 𝕜] [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} [LinearOrderedField 𝕜] [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
@[simp]
theorem iccHomeoI_apply_coe {𝕜 : Type u_1} [LinearOrderedField 𝕜] [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} [LinearOrderedField 𝕜] [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
@[simp]
theorem unitInterval.coe_toNNReal (x : unitInterval) :
(toNNReal x) = x