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

@[inline, reducible]

abbrev unitInterval : Set ℝ

The unit interval [0,1] in ℝ.

Equations

• unitInterval = Set.Icc 0 1

def unitInterval.termI : Lean.ParserDescr

The unit interval [0,1] in ℝ.

Equations

• unitInterval.termI = Lean.ParserDescr.node `unitInterval.termI 1024 (Lean.ParserDescr.symbol "I")

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.mem_iff_one_sub_mem {t : ℝ} : t ∈ unitInterval ↔ 1 - t ∈ unitInterval

instance unitInterval.hasZero : Zero ↑unitInterval

Equations

• unitInterval.hasZero = { zero := { val := 0, property := unitInterval.zero_mem } }

instance unitInterval.hasOne : One ↑unitInterval

Equations

• unitInterval.hasOne = { one := { val := 1, property := unitInterval.hasOne.proof_1 } }

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

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

instance unitInterval.instNonemptyElemRealUnitInterval : Nonempty ↑unitInterval

Equations

• unitInterval.instNonemptyElemRealUnitInterval = unitInterval.instNonemptyElemRealUnitInterval.proof_1

instance unitInterval.instMulElemRealUnitInterval : Mul ↑unitInterval

Equations

• unitInterval.instMulElemRealUnitInterval = { mul := fun x y => { val := ↑x * ↑y, property := (_ : ↑x * ↑y ∈ unitInterval) } }

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

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

def unitInterval.symm : ↑unitInterval → ↑unitInterval

Unit interval central symmetry.

Equations

• unitInterval.symm t = { val := 1 - ↑t, property := (_ : 1 - ↑t ∈ unitInterval) }

def unitInterval.termσ : Lean.ParserDescr

Unit interval central symmetry.

Equations

• unitInterval.termσ = Lean.ParserDescr.node `unitInterval.termσ 1024 (Lean.ParserDescr.symbol "σ")

@[simp]

theorem unitInterval.symm_zero : unitInterval.symm 0 = 1

@[simp]

theorem unitInterval.symm_one : unitInterval.symm 1 = 0

@[simp]

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

@[simp]

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

theorem unitInterval.continuous_symm : Continuous unitInterval.symm

instance unitInterval.instConnectedSpaceElemRealUnitIntervalInstTopologicalSpaceSubtypeMemSetInstMembershipSetToTopologicalSpaceToUniformSpacePseudoMetricSpace : ConnectedSpace ↑unitInterval

Equations

• One or more equations did not get rendered due to their size.

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.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

@[simp]

theorem projIcc_eq_zero {x : ℝ} : Set.projIcc 0 1 (_ : 0 ≤ 1) x = 0 ↔ x ≤ 0

@[simp]

theorem projIcc_eq_one {x : ℝ} : Set.projIcc 0 1 (_ : 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.

Equations

• Tactic.Interactive.tacticUnit_interval = Lean.ParserDescr.node `Tactic.Interactive.tacticUnit_interval 1024 (Lean.ParserDescr.nonReservedSymbol "unit_interval" false)

theorem affineHomeomorph_image_I {𝕜 : Type u_1} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] (a : 𝕜) (b : 𝕜) (h : 0 < a) : ↑(affineHomeomorph a b (_ : a ≠ 0)) '' 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} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] (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

• One or more equations did not get rendered due to their size.

@[simp]

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