mathlib3 documentation

topology.unit_interval

The unit interval, as a topological space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

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]
@[protected, instance]
Equations

Unit interval central symmetry.

Equations
theorem unit_interval.add_pos {t : unit_interval} {x : } (hx : 0 < x) :
0 < x + t

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) :
@[simp]
theorem proj_Icc_eq_zero {x : } :
@[simp]
theorem proj_Icc_eq_one {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} [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