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 #

source

@[inline, reducible]

abbrev unitInterval :

Set ℝ

The unit interval [0,1] in ℝ.

Instances For

source

def unitInterval.termI :

Lean.ParserDescr

The unit interval [0,1] in ℝ.

Instances For

source

theorem unitInterval.zero_mem :

0 ∈ unitInterval

source

theorem unitInterval.one_mem :

1 ∈ unitInterval

source

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

x * y ∈ unitInterval

source

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

x / y ∈ unitInterval

source

theorem unitInterval.fract_mem (x : ℝ) :

Int.fract x ∈ unitInterval

source

theorem unitInterval.mem_iff_one_sub_mem {t : ℝ} :

t ∈ unitInterval ↔ 1 - t ∈ unitInterval

source

instance unitInterval.hasZero :

Zero ↑unitInterval

source

instance unitInterval.hasOne :

One ↑unitInterval

source

theorem unitInterval.coe_ne_zero {x : ↑unitInterval} :

↑x ≠ 0 ↔ x ≠ 0

source

theorem unitInterval.coe_ne_one {x : ↑unitInterval} :

↑x ≠ 1 ↔ x ≠ 1

source

instance unitInterval.instNonemptyElemRealUnitInterval :

Nonempty ↑unitInterval

source

instance unitInterval.instMulElemRealUnitInterval :

Mul ↑unitInterval

source

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

x * y ≤ x

source

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

x * y ≤ y

source

def unitInterval.symm :

↑unitInterval → ↑unitInterval

Unit interval central symmetry.

Instances For

source

def unitInterval.termσ :

Lean.ParserDescr

Unit interval central symmetry.

Instances For

source

@[simp]

theorem unitInterval.symm_zero :

unitInterval.symm 0 = 1

source

@[simp]

theorem unitInterval.symm_one :

unitInterval.symm 1 = 0

source

@[simp]

theorem unitInterval.symm_symm (x : ↑unitInterval) :

unitInterval.symm (unitInterval.symm x) = x

source

@[simp]

theorem unitInterval.coe_symm_eq (x : ↑unitInterval) :

↑(unitInterval.symm x) = 1 - ↑x

source

theorem unitInterval.continuous_symm :

Continuous unitInterval.symm

source

instance unitInterval.instConnectedSpaceElemRealUnitIntervalInstTopologicalSpaceSubtypeMemSetInstMembershipSetToTopologicalSpaceToUniformSpacePseudoMetricSpace :

ConnectedSpace ↑unitInterval

source

theorem unitInterval.nonneg (x : ↑unitInterval) :

0 ≤ ↑x

source

theorem unitInterval.one_minus_nonneg (x : ↑unitInterval) :

0 ≤ 1 - ↑x

source

theorem unitInterval.le_one (x : ↑unitInterval) :

↑x ≤ 1

source

theorem unitInterval.one_minus_le_one (x : ↑unitInterval) :

1 - ↑x ≤ 1

source

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

0 < x + ↑t

source

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

0 ≤ t

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

source

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

t ≤ 1

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

source

theorem unitInterval.mul_pos_mem_iff {a : ℝ} {t : ℝ} (ha : 0 < a) :

a * t ∈ unitInterval ↔ t ∈ Set.Icc 0 (1 / a)

source

theorem unitInterval.two_mul_sub_one_mem_iff {t : ℝ} :

2 * t - 1 ∈ unitInterval ↔ t ∈ Set.Icc (1 / 2) 1

source

@[simp]

theorem projIcc_eq_zero {x : ℝ} :

Set.projIcc 0 1 (_ : 0 ≤ 1) x = 0 ↔ x ≤ 0

source

@[simp]

theorem projIcc_eq_one {x : ℝ} :

Set.projIcc 0 1 (_ : 0 ≤ 1) x = 1 ↔ 1 ≤ x

source

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.

Instances For

source

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

source

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

Instances For

source

@[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)

source

@[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