mathlib documentation

topology.unit_interval

The unit interval, as a topological space #

Use open_locale unit_interval 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 #

The unit interval [0,1] in ℝ.

@[instance]
Equations
@[simp]
theorem unit_interval.coe_zero  :
0 = 0
@[simp]
theorem unit_interval.mk_zero (h : 0 set.Icc 0 1) :
0, h⟩ = 0
@[instance]
Equations
@[simp]
theorem unit_interval.coe_one  :
1 = 1
@[simp]
theorem unit_interval.mk_one (h : 1 set.Icc 0 1) :
1, h⟩ = 1

Unit interval central symmetry.

Equations
theorem unit_interval.mul_pos_mem_iff {a t : } (ha : 0 < a) :

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

theorem affine_homeomorph_image_I {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [topological_ring 𝕜] (a b : 𝕜) (h : 0 < a) :

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

def Icc_homeo_I {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [topological_ring 𝕜] (a b : 𝕜) (h : a < b) :

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

Equations
@[simp]
theorem Icc_homeo_I_apply_coe {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [topological_ring 𝕜] (a b : 𝕜) (h : a < b) (x : (set.Icc a b)) :
((Icc_homeo_I a b h) x) = (x - a) / (b - a)
@[simp]
theorem Icc_homeo_I_symm_apply_coe {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [topological_ring 𝕜] (a b : 𝕜) (h : a < b) (x : (set.Icc 0 1)) :
(((Icc_homeo_I a b h).symm) x) = (b - a) * x + a