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 : Set ℝ

The unit interval [0,1] in ℝ.

def unitInterval.termI : Lean.ParserDescr

The unit interval [0,1] in ℝ.

theorem unitInterval.zero_mem : 0 ∈ unitInterval

theorem unitInterval.one_mem : 1 ∈ unitInterval

theorem unitInterval.mul_mem {x y : ℝ} (hx : x ∈ unitInterval) (hy : y ∈ unitInterval) : x * y ∈ unitInterval

theorem unitInterval.div_mem {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : x ≤ y) : x / y ∈ unitInterval

theorem unitInterval.fract_mem (x : ℝ) : Int.fract x ∈ unitInterval

theorem unitInterval.univ_eq_Icc : Set.univ = Set.Icc 0 1

theorem unitInterval.coe_ne_zero {x : ↑unitInterval} : ↑x ≠ 0 ↔ x ≠ 0

theorem unitInterval.coe_ne_one {x : ↑unitInterval} : ↑x ≠ 1 ↔ x ≠ 1

@[simp]

theorem unitInterval.coe_pos {x : ↑unitInterval} : 0 < ↑x ↔ 0 < x

@[simp]

theorem unitInterval.coe_lt_one {x : ↑unitInterval} : ↑x < 1 ↔ x < 1

theorem unitInterval.mul_le_left {x y : ↑unitInterval} : x * y ≤ x

theorem unitInterval.mul_le_right {x y : ↑unitInterval} : x * y ≤ y

theorem unitInterval.eq_closedBall : unitInterval = Metric.closedBall 2⁻¹ 2⁻¹

def unitInterval.symm : ↑unitInterval → ↑unitInterval

Unit interval central symmetry.

def unitInterval.termσ : Lean.ParserDescr

Unit interval central symmetry.

@[simp]

theorem unitInterval.symm_zero : symm 0 = 1

@[simp]

theorem unitInterval.symm_one : symm 1 = 0

@[simp]

theorem unitInterval.symm_symm (x : ↑unitInterval) : symm (symm x) = x

theorem unitInterval.symm_involutive : Function.Involutive symm

theorem unitInterval.symm_bijective : Function.Bijective symm

@[simp]

theorem unitInterval.coe_symm_eq (x : ↑unitInterval) : ↑(symm x) = 1 - ↑x

theorem unitInterval.image_coe_preimage_symm {s : Set ↑unitInterval} : Subtype.val '' (symm ⁻¹' s) = (fun (x : ℝ) => 1 - x) ⁻¹' (Subtype.val '' s)

@[simp]

theorem unitInterval.symm_projIcc (x : ℝ) : symm (Set.projIcc 0 1 ⋯ x) = Set.projIcc 0 1 ⋯ (1 - x)

theorem unitInterval.continuous_symm : Continuous symm

def unitInterval.symmHomeomorph : ↑unitInterval ≃ₜ ↑unitInterval

unitInterval.symm as a Homeomorph.

@[simp]

theorem unitInterval.symmHomeomorph_apply (a✝ : ↑unitInterval) : symmHomeomorph a✝ = symm a✝

@[simp]

theorem unitInterval.symmHomeomorph_symm_apply (a✝ : ↑unitInterval) : symmHomeomorph.symm a✝ = symm a✝

theorem unitInterval.strictAnti_symm : StrictAnti symm

@[simp]

theorem unitInterval.symm_inj {i j : ↑unitInterval} : symm i = symm j ↔ i = j

theorem unitInterval.half_le_symm_iff (t : ↑unitInterval) : 1 / 2 ≤ ↑(symm t) ↔ ↑t ≤ 1 / 2

@[simp]

theorem unitInterval.symm_eq_one {i : ↑unitInterval} : symm i = 1 ↔ i = 0

@[simp]

theorem unitInterval.symm_eq_zero {i : ↑unitInterval} : symm i = 0 ↔ i = 1

@[simp]

theorem unitInterval.symm_le_symm {i j : ↑unitInterval} : symm i ≤ symm j ↔ j ≤ i

theorem unitInterval.le_symm_comm {i j : ↑unitInterval} : i ≤ symm j ↔ j ≤ symm i

theorem unitInterval.symm_le_comm {i j : ↑unitInterval} : symm i ≤ j ↔ symm j ≤ i

@[simp]

theorem unitInterval.symm_lt_symm {i j : ↑unitInterval} : symm i < symm j ↔ j < i

theorem unitInterval.lt_symm_comm {i j : ↑unitInterval} : i < symm j ↔ j < symm i

theorem unitInterval.symm_lt_comm {i j : ↑unitInterval} : symm i < j ↔ symm j < i

instance unitInterval.instConnectedSpaceElemReal : ConnectedSpace ↑unitInterval

theorem unitInterval.nonneg (x : ↑unitInterval) : 0 ≤ ↑x

theorem unitInterval.one_minus_nonneg (x : ↑unitInterval) : 0 ≤ 1 - ↑x

theorem unitInterval.le_one (x : ↑unitInterval) : ↑x ≤ 1

theorem unitInterval.one_minus_le_one (x : ↑unitInterval) : 1 - ↑x ≤ 1

theorem unitInterval.add_pos {t : ↑unitInterval} {x : ℝ} (hx : 0 < x) : 0 < x + ↑t

theorem unitInterval.nonneg' {t : ↑unitInterval} : 0 ≤ t

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

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

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

theorem unitInterval.pos_iff_ne_zero {x : ↑unitInterval} : 0 < x ↔ x ≠ 0

theorem unitInterval.lt_one_iff_ne_one {x : ↑unitInterval} : x < 1 ↔ x ≠ 1

theorem unitInterval.eq_one_or_eq_zero_of_le_mul {i j : ↑unitInterval} (h : i ≤ j * i) : i = 0 ∨ j = 1

instance unitInterval.instNontrivialElemReal : Nontrivial ↑unitInterval

theorem unitInterval.mul_pos_mem_iff {a t : ℝ} (ha : 0 < a) : a * t ∈ unitInterval ↔ t ∈ Set.Icc 0 (1 / a)

theorem unitInterval.two_mul_sub_one_mem_iff {t : ℝ} : 2 * t - 1 ∈ unitInterval ↔ t ∈ Set.Icc (1 / 2) 1

def unitInterval.submonoid : Submonoid ℝ

The unit interval as a submonoid of ℝ.

@[simp]

theorem unitInterval.coe_unitIntervalSubmonoid : ↑submonoid = unitInterval

@[simp]

theorem unitInterval.mem_unitIntervalSubmonoid {x : ℝ} : x ∈ submonoid ↔ x ∈ unitInterval

theorem unitInterval.prod_mem {ι : Type u_1} {t : Finset ι} {f : ι → ℝ} (h : ∀ c ∈ t, f c ∈ unitInterval) : ∏ c ∈ t, f c ∈ unitInterval

@[implicit_reducible]

noncomputable instance unitInterval.instLinearOrderedCommMonoidWithZeroElemReal : LinearOrderedCommMonoidWithZero ↑unitInterval

theorem unitInterval.subtype_Iic_eq_Icc (x : ↑unitInterval) : Subtype.val ⁻¹' Set.Iic ↑x = Set.Icc 0 x

theorem unitInterval.subtype_Iio_eq_Ico (x : ↑unitInterval) : Subtype.val ⁻¹' Set.Iio ↑x = Set.Ico 0 x

theorem unitInterval.subtype_Ici_eq_Icc (x : ↑unitInterval) : Subtype.val ⁻¹' Set.Ici ↑x = Set.Icc x 1

theorem unitInterval.subtype_Ioi_eq_Ioc (x : ↑unitInterval) : Subtype.val ⁻¹' Set.Ioi ↑x = Set.Ioc x 1

theorem Set.abs_projIcc_sub_projIcc {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b c d : α} (h : a ≤ b) : |↑(projIcc a b h c) - ↑(projIcc a b h d)| ≤ |c - d|

Set.projIcc is a contraction.

def Set.Icc.addNSMul {α : Type u_1} [AddCommGroup α] [LinearOrder α] {a b : α} (h : a ≤ b) (δ : α) (n : ℕ) : ↑(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.

theorem Set.Icc.addNSMul_zero {α : Type u_1} [AddCommGroup α] [LinearOrder α] {a b : α} (h : a ≤ b) {δ : α} : ↑(addNSMul h δ 0) = a

theorem Set.Icc.addNSMul_eq_right {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a ≤ b) {δ : α} [Archimedean α] (hδ : 0 < δ) : ∃ (m : ℕ), ∀ n ≥ m, ↑(addNSMul h δ n) = b

theorem Set.Icc.monotone_addNSMul {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a ≤ b) {δ : α} (hδ : 0 ≤ δ) : Monotone (addNSMul h δ)

theorem Set.Icc.abs_sub_addNSMul_le {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b : α} (h : a ≤ b) {δ : α} (hδ : 0 ≤ δ) {t : ↑(Icc a b)} (n : ℕ) (ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))) : |↑t - ↑(addNSMul h δ n)| ≤ δ

def Set.Icc.convexCombo {a b : ℝ} (x y : ↑(Icc a b)) (t : ↑unitInterval) : ↑(Icc a b)

Form a convex linear combination of two points in a closed interval.

This should be removed once a general theory of convex spaces is available in Mathlib.

@[simp]

theorem Set.Icc.coe_convexCombo {a b : ℝ} (x y : ↑(Icc a b)) (t : ↑unitInterval) : ↑(convexCombo x y t) = (1 - ↑t) * ↑x + ↑t * ↑y

@[simp]

theorem Set.Icc.convexCombo_zero {a b : ℝ} (x y : ↑(Icc a b)) : convexCombo x y 0 = x

@[simp]

theorem Set.Icc.convexCombo_one {a b : ℝ} (x y : ↑(Icc a b)) : convexCombo x y 1 = y

@[simp]

theorem Set.Icc.convexCombo_zero_one (t : ↑unitInterval) : convexCombo 0 1 t = t

@[simp]

theorem Set.Icc.convexCombo_eq {a b : ℝ} (x : ↑(Icc a b)) (t : ↑unitInterval) : convexCombo x x t = x

@[simp]

theorem Set.Icc.convexCombo_symm {a b : ℝ} (x y : ↑(Icc a b)) (t : ↑unitInterval) : convexCombo x y (unitInterval.symm t) = convexCombo y x t

theorem Set.Icc.le_convexCombo {a b : ℝ} {x y : ↑(Icc a b)} (h : x ≤ y) (t : ↑unitInterval) : x ≤ convexCombo x y t

theorem Set.Icc.convexCombo_le {a b : ℝ} {x y : ↑(Icc a b)} (h : x ≤ y) (t : ↑unitInterval) : convexCombo x y t ≤ y

theorem Set.Icc.continuous_convexCombo {a b : ℝ} (x y : ↑(Icc a b)) : Continuous (convexCombo x y)

theorem Set.Icc.continuous_convexCombo_prod {a b : ℝ} : Continuous fun (x : ↑(Icc a b) × ↑(Icc a b) × ↑unitInterval) => convexCombo x.1 x.2.1 x.2.2

@[reducible, inline]

noncomputable abbrev Set.Icc.convexCombo_assoc_coeff₁ (s t : ↑unitInterval) : ↑unitInterval

Helper definition for convexCombo_assoc, giving one of the coefficients appearing when we reassociate a convex combination.

@[reducible, inline]

abbrev Set.Icc.convexCombo_assoc_coeff₂ (s t : ↑unitInterval) : ↑unitInterval

Helper definition for convexCombo_assoc, giving one of the coefficients appearing when we reassociate a convex combination.

theorem Set.Icc.convexCombo_assoc {a b : ℝ} (x y z : ↑(Icc a b)) (s t : ↑unitInterval) : convexCombo x (convexCombo y z t) s = convexCombo (convexCombo x y (convexCombo_assoc_coeff₁ s t)) z (convexCombo_assoc_coeff₂ s t)

@[reducible, inline]

abbrev Set.Icc.convexCombo_assoc_coeff₁' (s t : ↑unitInterval) : ↑unitInterval

Helper definition for convexCombo_assoc', giving one of the coefficients appearing when we reassociate a convex combination in the reverse direction.

@[reducible, inline]

noncomputable abbrev Set.Icc.convexCombo_assoc_coeff₂' (s t : ↑unitInterval) : ↑unitInterval

Helper definition for convexCombo_assoc', giving one of the coefficients appearing when we reassociate a convex combination in the reverse direction.

theorem Set.Icc.convexCombo_assoc' {a b : ℝ} (x y z : ↑(Icc a b)) (s t : ↑unitInterval) : convexCombo (convexCombo x y s) z t = convexCombo x (convexCombo y z (convexCombo_assoc_coeff₂' s t)) (convexCombo_assoc_coeff₁' s t)

theorem Set.Icc.eq_convexCombo {a b : ℝ} {x y z : ↑(Icc a b)} (hxy : x ≤ y) (hyz : y ≤ z) : y = convexCombo x z ⟨(↑y - ↑x) / (↑z - ↑x), ⋯⟩

A point between two points in a closed interval can be expressed as a convex combination of them.

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 ∧ Monotone t ∧ (∃ (m : ℕ), ∀ n ≥ m, ↑(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 : ι → Set ↑unitInterval} (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : Set.univ ⊆ ⋃ (i : ι), c i) : ∃ (t : ℕ → ↑unitInterval), t 0 = 0 ∧ Monotone t ∧ (∃ (n : ℕ), ∀ m ≥ n, 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 : ι → Set (↑unitInterval × ↑unitInterval)} (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : Set.univ ⊆ ⋃ (i : ι), c i) : ∃ (t : ℕ → ↑unitInterval), t 0 = 0 ∧ Monotone t ∧ (∃ (n : ℕ), ∀ m ≥ n, 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

def Tactic.Interactive.tacticUnit_interval : Lean.ParserDescr

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

theorem affineHomeomorph_image_I {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b : 𝕜) (h : 0 < a) : ⇑(affineHomeomorph a b ⋯) '' 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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (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].

@[simp]

theorem iccHomeoI_apply_coe {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (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} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b : 𝕜) (h : a < b) (x : ↑(Set.Icc 0 1)) : ↑((iccHomeoI a b h).symm x) = (b - a) * ↑x + a

def unitInterval.toNNReal : ↑unitInterval → NNReal

The coercion from I to ℝ≥0.

@[simp]

theorem unitInterval.toNNReal_zero : toNNReal 0 = 0

@[simp]

theorem unitInterval.toNNReal_one : toNNReal 1 = 1

theorem unitInterval.toNNReal_continuous : Continuous toNNReal

@[simp]

theorem unitInterval.coe_toNNReal (x : ↑unitInterval) : ↑(toNNReal x) = ↑x

@[simp]

theorem unitInterval.toNNReal_add_toNNReal_symm (x : ↑unitInterval) : toNNReal x + toNNReal (symm x) = 1

@[simp]

theorem unitInterval.toNNReal_symm_add_toNNReal (x : ↑unitInterval) : toNNReal (symm x) + toNNReal x = 1