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 #

source
@[reducible]
def unit_interval  :
set ℝ

The unit interval [0,1] in ℝ.

source
theorem unit_interval.zero_mem  :
0 ∈ unit_interval
source
theorem unit_interval.one_mem  :
1 ∈ unit_interval
source
theorem unit_interval.mul_mem {x y : ℝ} (hx : x ∈ unit_interval) (hy : y ∈ unit_interval) :
x * y ∈ unit_interval
source
theorem unit_interval.div_mem {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : x ≤ y) :
x / y ∈ unit_interval
source
theorem unit_interval.fract_mem (x : ℝ) :
int.fract x ∈ unit_interval
source
theorem unit_interval.mem_iff_one_sub_mem {t : ℝ} :
t ∈ unit_interval ↔ 1 - t ∈ unit_interval
source
@[protected, instance]
def unit_interval.has_zero  :
has_zero ↥unit_interval
Equations
source
@[protected, instance]
def unit_interval.has_one  :
has_one ↥unit_interval
Equations
source
theorem unit_interval.coe_ne_zero {x : ↥unit_interval} :
↑x ≠ 0 ↔ x ≠ 0
source
theorem unit_interval.coe_ne_one {x : ↥unit_interval} :
↑x ≠ 1 ↔ x ≠ 1
source
@[protected, instance]
def unit_interval.nonempty  :
nonempty ↥unit_interval
source
@[protected, instance]
def unit_interval.has_mul  :
has_mul ↥unit_interval
Equations
source
theorem unit_interval.mul_le_left {x y : ↥unit_interval} :
x * y ≤ x
source
theorem unit_interval.mul_le_right {x y : ↥unit_interval} :
x * y ≤ y
source
def unit_interval.symm  :
↥unit_interval → ↥unit_interval

Unit interval central symmetry.

Equations
source
@[simp]
theorem unit_interval.symm_zero  :
unit_interval.symm 0 = 1
source
@[simp]
theorem unit_interval.symm_one  :
unit_interval.symm 1 = 0
source
@[simp]
theorem unit_interval.symm_symm (x : ↥unit_interval) :
unit_interval.symm (unit_interval.symm x) = x
source
@[simp]
theorem unit_interval.coe_symm_eq (x : ↥unit_interval) :
↑(unit_interval.symm x) = 1 - ↑x
source
@[continuity]
theorem unit_interval.continuous_symm  :
continuous unit_interval.symm
source
@[protected, instance]
def unit_interval.connected_space  :
connected_space ↥unit_interval
source
theorem unit_interval.nonneg (x : ↥unit_interval) :
0 ≤ ↑x
source
theorem unit_interval.one_minus_nonneg (x : ↥unit_interval) :
0 ≤ 1 - ↑x
source
theorem unit_interval.le_one (x : ↥unit_interval) :
↑x ≤ 1
source
theorem unit_interval.one_minus_le_one (x : ↥unit_interval) :
1 - ↑x ≤ 1
source
theorem unit_interval.add_pos {t : ↥unit_interval} {x : ℝ} (hx : 0 < x) :
0 < x + ↑t
source
theorem unit_interval.nonneg' {t : ↥unit_interval} :
0 ≤ t

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

source
theorem unit_interval.le_one' {t : ↥unit_interval} :
t ≤ 1

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

source
theorem unit_interval.mul_pos_mem_iff {a t : ℝ} (ha : 0 < a) :
a * t ∈ unit_interval ↔ t ∈ set.Icc 0 (1 / a)
source
theorem unit_interval.two_mul_sub_one_mem_iff {t : ℝ} :
2 * t - 1 ∈ unit_interval ↔ t ∈ set.Icc (1 / 2) 1
source
@[simp]
theorem proj_Icc_eq_zero {x : ℝ} :
set.proj_Icc 0 1 zero_le_one x = 0 ↔ x ≤ 0
source
@[simp]
theorem proj_Icc_eq_one {x : ℝ} :
set.proj_Icc 0 1 zero_le_one x = 1 ↔ 1 ≤ x
source
meta def tactic.interactive.unit_interval  :
tactic unit

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

source
theorem affine_homeomorph_image_I {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [topological_ring 𝕜] (a b : 𝕜) (h : 0 < a) :
⇑(affine_homeomorph a b _) '' set.Icc 0 1 = set.Icc b (a + b)

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

source
def Icc_homeo_I {𝕜 : Type u_1} [linear_ordered_field 𝕜] [topological_space 𝕜] [topological_ring 𝕜] (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
source
@[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)
source
@[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