# 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]
abbrev unitInterval :

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 : ) (hy : ) :
theorem unitInterval.div_mem {x : } {y : } (hx : 0 x) (hy : 0 y) (hxy : x y) :
Equations
Equations
theorem unitInterval.coe_ne_zero {x : } :
x 0 x 0
theorem unitInterval.coe_ne_one {x : } :
x 1 x 1
Equations
Equations
theorem unitInterval.mul_le_left {x : } {y : } :
x * y x
theorem unitInterval.mul_le_right {x : } {y : } :
x * y y

Unit interval central symmetry.

Equations
• = 1 - t,
Instances For

Unit interval central symmetry.

Equations
Instances For
@[simp]
@[simp]
theorem unitInterval.symm_symm (x : ) :
@[simp]
theorem unitInterval.coe_symm_eq (x : ) :
= 1 - x
@[simp]
@[simp]
theorem unitInterval.symmHomeomorph_apply :
∀ (a : ), unitInterval.symmHomeomorph a =

unitInterval.symm as a Homeomorph.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[deprecated unitInterval.symm_involutive]

Alias of unitInterval.symm_involutive.

@[deprecated unitInterval.symm_bijective]

Alias of unitInterval.symm_bijective.

theorem unitInterval.half_le_symm_iff (t : ) :
1 / 2 t 1 / 2
theorem unitInterval.nonneg (x : ) :
0 x
theorem unitInterval.one_minus_nonneg (x : ) :
0 1 - x
theorem unitInterval.le_one (x : ) :
x 1
theorem unitInterval.one_minus_le_one (x : ) :
1 - x 1
theorem unitInterval.add_pos {t : } {x : } (hx : 0 < x) :
0 < x + t
theorem unitInterval.nonneg' {t : } :
0 t

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

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

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

Equations
theorem unitInterval.mul_pos_mem_iff {a : } {t : } (ha : 0 < a) :
a * t unitInterval t Set.Icc 0 (1 / a)
theorem Set.abs_projIcc_sub_projIcc {α : Type u_1} {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} {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} {a : α} {b : α} (h : a b) {δ : α} :
() = a
theorem Set.Icc.addNSMul_eq_right {α : Type u_1} {a : α} {b : α} (h : a b) {δ : α} [] (hδ : 0 < δ) :
∃ (m : ), nm, () = b
theorem Set.Icc.monotone_addNSMul {α : Type u_1} {a : α} {b : α} (h : a b) {δ : α} (hδ : 0 δ) :
theorem Set.Icc.abs_sub_addNSMul_le {α : Type u_1} {a : α} {b : α} (h : a b) {δ : α} (hδ : 0 δ) {t : (Set.Icc a b)} (n : ) (ht : t Set.Icc () (Set.Icc.addNSMul h δ (n + 1))) :
|t - ()| δ
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 (∃ (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 : ι} (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : Set.univ ⋃ (i : ι), c i) :
∃ (t : ), t 0 = 0 (∃ (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 : ι} (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : Set.univ ⋃ (i : ι), c i) :
∃ (t : ), t 0 = 0 (∃ (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} [] [] (a : 𝕜) (b : 𝕜) (h : 0 < a) :
() '' 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} [] [] (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} [] [] (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} [] [] (a : 𝕜) (b : 𝕜) (h : a < b) (x : (Set.Icc 0 1)) :
((iccHomeoI a b h).symm x) = (b - a) * x + a