# mathlibdocumentation

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 #

@[reducible]
def unit_interval  :

The unit interval [0,1] in ℝ.

theorem unit_interval.div_mem {x y : } (hx : 0 x) (hy : 0 y) (hxy : x y) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations

Unit interval central symmetry.

Equations
@[simp]
@[simp]
@[simp]
@[continuity]
@[protected, instance]

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

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

theorem unit_interval.mul_pos_mem_iff {a t : } (ha : 0 < a) :
a * t unit_interval t (1 / a)
@[simp]
theorem proj_Icc_eq_zero {x : } :
x = 0 x 0
@[simp]
theorem proj_Icc_eq_one {x : } :
x = 1 1 x

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} (a b : 𝕜) (h : 0 < a) :
_) '' 1 = (a + b)

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

def Icc_homeo_I {𝕜 : Type u_1} (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} (a b : 𝕜) (h : a < b) (x : (set.Icc a b)) :
( b h) x) = (x - a) / (b - a)
@[simp]
theorem Icc_homeo_I_symm_apply_coe {𝕜 : Type u_1} (a b : 𝕜) (h : a < b) (x : (set.Icc 0 1)) :
(((Icc_homeo_I a b h).symm) x) = (b - a) * x + a