Mathlib.Topology.UnitInterval

unitInterval abbrev

: Set ℝ

Full source

/-- The unit interval `[0,1]` in ℝ. -/
abbrev unitInterval : Set ℝ :=
  Set.Icc 0 1

Unit Interval $[0,1]$ in $\mathbb{R}$

Informal description

The unit interval is the closed interval $[0, 1]$ in the real numbers, denoted as $I := \{x \in \mathbb{R} \mid 0 \leq x \leq 1\}$.

unitInterval.termI definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped[unitInterval] notation "I" => unitInterval

Unit interval notation `I` for `[0,1]`

Informal description

The notation `I` is introduced to represent the closed unit interval `[0, 1]` in the real numbers.

unitInterval.zero_mem theorem

: (0 : ℝ) ∈ I

Full source

theorem zero_mem : (0 : ℝ) ∈ I :=
  ⟨le_rfl, zero_le_one⟩

Zero Belongs to the Unit Interval

Informal description

The real number $0$ is an element of the unit interval $I = [0, 1]$, i.e., $0 \in I$.

unitInterval.one_mem theorem

: (1 : ℝ) ∈ I

Full source

theorem one_mem : (1 : ℝ) ∈ I :=
  ⟨zero_le_one, le_rfl⟩

One Belongs to the Unit Interval

Informal description

The real number $1$ is an element of the unit interval $I = [0, 1]$, i.e., $1 \in I$.

unitInterval.mul_mem theorem

{x y : ℝ} (hx : x ∈ I) (hy : y ∈ I) : x * y ∈ I

Full source

theorem mul_mem {x y : ℝ} (hx : x ∈ I) (hy : y ∈ I) : x * y ∈ I :=
  ⟨mul_nonneg hx.1 hy.1, mul_le_one₀ hx.2 hy.1 hy.2⟩

Closure of Unit Interval under Multiplication

Informal description

For any real numbers $x, y \in [0, 1]$, their product $x \cdot y$ also belongs to the unit interval $[0, 1]$.

unitInterval.div_mem theorem

{x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : x ≤ y) : x / y ∈ I

Full source

theorem div_mem {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : x ≤ y) : x / y ∈ I :=
  ⟨div_nonneg hx hy, div_le_one_of_le₀ hxy hy⟩

Ratio of Nonnegative Reals in Unit Interval under Dominance Condition

Informal description

For any real numbers $x$ and $y$ such that $0 \leq x$, $0 \leq y$, and $x \leq y$, the ratio $x / y$ belongs to the unit interval $I = [0, 1]$.

unitInterval.fract_mem theorem

(x : ℝ) : fract x ∈ I

Full source

theorem fract_mem (x : ℝ) : fractfract x ∈ I :=
  ⟨fract_nonneg _, (fract_lt_one _).le⟩

Fractional Part Lies in Unit Interval: $\operatorname{fract}(x) \in [0,1]$

Informal description

For any real number $x$, the fractional part $\operatorname{fract}(x) := x - \lfloor x \rfloor$ belongs to the unit interval $I = [0, 1]$.

unitInterval.mem_iff_one_sub_mem theorem

{t : ℝ} : t ∈ I ↔ 1 - t ∈ I

Full source

theorem mem_iff_one_sub_mem {t : ℝ} : t ∈ It ∈ I ↔ 1 - t ∈ I := by
  rw [mem_Icc, mem_Icc]
  constructor <;> intro <;> constructor <;> linarith

Characterization of Unit Interval Membership via $1-t$

Informal description

For any real number $t$, $t$ belongs to the unit interval $I = [0,1]$ if and only if $1 - t$ belongs to $I$.

unitInterval.hasZero instance

: Zero I

Full source

instance hasZero : Zero I :=
  ⟨⟨0, zero_mem⟩⟩

The Zero Element of the Unit Interval

Informal description

The unit interval $I = [0,1]$ has a distinguished element $0$ (the left endpoint).

unitInterval.hasOne instance

: One I

Full source

instance hasOne : One I :=
  ⟨⟨1, by constructor <;> norm_num⟩⟩

The Unit Interval Has a One Element

Informal description

The unit interval $I = [0,1]$ has a distinguished element $1$ (the right endpoint).

unitInterval.instZeroLEOneClassElemReal instance

: ZeroLEOneClass I

Full source

instance : ZeroLEOneClass I := ⟨zero_le_one (α := ℝ)⟩

Zero is Less Than or Equal to One in the Unit Interval

Informal description

The unit interval $I = [0,1]$ satisfies the condition $0 \leq 1$ in its ordered structure.

unitInterval.instCompleteLatticeElemReal instance

: CompleteLattice I

Full source

instance : CompleteLattice I := have : Fact ((0 : ℝ) ≤ 1) := ⟨zero_le_one⟩; inferInstance

Complete Lattice Structure on the Unit Interval

Informal description

The unit interval $I = [0,1]$ has a complete lattice structure.

unitInterval.univ_eq_Icc theorem

: (univ : Set I) = Icc (0 : I) (1 : I)

Full source

lemma univ_eq_Icc : (univ : Set I) = Icc (0 : I) (1 : I) := Icc_bot_top.symm

Universal Set of Unit Interval Equals Closed Interval $[0,1]$

Informal description

The universal set of the unit interval $I = [0,1]$ is equal to the closed interval from $0$ to $1$ within $I$, i.e., $\mathrm{univ} = [0, 1]$.

unitInterval.coe_ne_zero theorem

{x : I} : (x : ℝ) ≠ 0 ↔ x ≠ 0

Full source

@[norm_cast] theorem coe_ne_zero {x : I} : (x : ℝ) ≠ 0(x : ℝ) ≠ 0 ↔ x ≠ 0 := coe_eq_zero.not

Nonzero Criterion for Unit Interval Elements: $x \neq 0$ in $I$ iff $x \neq 0$ in $\mathbb{R}$

Informal description

For any element $x$ in the unit interval $I = [0,1]$, the real number corresponding to $x$ is nonzero if and only if $x$ is not equal to the zero element of $I$.

unitInterval.coe_ne_one theorem

{x : I} : (x : ℝ) ≠ 1 ↔ x ≠ 1

Full source

@[norm_cast] theorem coe_ne_one {x : I} : (x : ℝ) ≠ 1(x : ℝ) ≠ 1 ↔ x ≠ 1 := coe_eq_one.not

Characterization of Non-Endpoint Elements in the Unit Interval via Real Embedding

Informal description

For any element $x$ in the unit interval $I = [0,1]$, the real number corresponding to $x$ is not equal to $1$ if and only if $x$ is not equal to the right endpoint $1$ of the interval.

unitInterval.coe_pos theorem

{x : I} : (0 : ℝ) < x ↔ 0 < x

Full source

@[simp, norm_cast] theorem coe_pos {x : I} : (0 : ℝ) < x ↔ 0 < x := Iff.rfl

Positivity Condition for Unit Interval Elements

Informal description

For any element $x$ in the unit interval $I = [0,1]$, the real number corresponding to $x$ is positive if and only if $x$ is not equal to $0$, i.e., $0 < x \leftrightarrow x \neq 0$.

unitInterval.coe_lt_one theorem

{x : I} : (x : ℝ) < 1 ↔ x < 1

Full source

@[simp, norm_cast] theorem coe_lt_one {x : I} : (x : ℝ) < 1 ↔ x < 1 := Iff.rfl

Characterization of Elements Less Than One in the Unit Interval

Informal description

For any element $x$ in the unit interval $I = [0, 1]$, the real number corresponding to $x$ is less than $1$ if and only if $x$ is not equal to the right endpoint $1$.

unitInterval.instNonemptyElemReal instance

: Nonempty I

Full source

instance : Nonempty I :=
  ⟨0⟩

Nonemptiness of the Unit Interval

Informal description

The unit interval $I = [0, 1]$ is nonempty.

unitInterval.instMulElemReal instance

: Mul I

Full source

instance : Mul I :=
  ⟨fun x y => ⟨x * y, mul_mem x.2 y.2⟩⟩

Multiplication on the Unit Interval

Informal description

The unit interval $I = [0, 1]$ is equipped with a multiplication operation, making it a multiplicative structure.

unitInterval.mul_le_left theorem

{x y : I} : x * y ≤ x

Full source

theorem mul_le_left {x y : I} : x * y ≤ x :=
  Subtype.coe_le_coe.mp <| mul_le_of_le_one_right x.2.1 y.2.2

Left Multiplication Bound in Unit Interval: $x \cdot y \leq x$ for $x, y \in [0,1]$

Informal description

For any two elements $x, y$ in the unit interval $I = [0,1]$, the product $x \cdot y$ is less than or equal to $x$.

unitInterval.mul_le_right theorem

{x y : I} : x * y ≤ y

Full source

theorem mul_le_right {x y : I} : x * y ≤ y :=
  Subtype.coe_le_coe.mp <| mul_le_of_le_one_left y.2.1 x.2.2

Right Multiplication Bound in Unit Interval: $x \cdot y \leq y$ for $x, y \in [0,1]$

Informal description

For any two elements $x, y$ in the unit interval $I = [0,1]$, the product $x \cdot y$ is less than or equal to $y$.

unitInterval.symm definition

: I → I

Full source

/-- Unit interval central symmetry. -/
def symm : I → I := fun t => ⟨1 - t, mem_iff_one_sub_mem.mp t.prop⟩

Central symmetry of the unit interval

Informal description

The function $\sigma : [0,1] \to [0,1]$ defined by $\sigma(t) = 1 - t$ is the central symmetry of the unit interval, mapping each point $t$ to its reflection across the midpoint $0.5$.

unitInterval.termσ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
scoped notation "σ" => unitInterval.symm

Notation for unit interval symmetry function

Informal description

The notation `σ` is defined as a shorthand for the function `unitInterval.symm`, which maps the unit interval `I = [0,1]` to itself.

unitInterval.symm_zero theorem

: σ 0 = 1

Full source

@[simp]
theorem symm_zero : σ 0 = 1 :=
  Subtype.ext <| by simp [symm]

Central Symmetry Maps Zero to One on the Unit Interval

Informal description

The central symmetry function $\sigma$ of the unit interval $[0,1]$, defined by $\sigma(t) = 1 - t$, maps the left endpoint $0$ to the right endpoint $1$, i.e., $\sigma(0) = 1$.

unitInterval.symm_one theorem

: σ 1 = 0

Full source

@[simp]
theorem symm_one : σ 1 = 0 :=
  Subtype.ext <| by simp [symm]

Central symmetry maps 1 to 0 in the unit interval

Informal description

The central symmetry function $\sigma$ of the unit interval $[0,1]$ satisfies $\sigma(1) = 0$.

unitInterval.symm_symm theorem

(x : I) : σ (σ x) = x

Full source

@[simp]
theorem symm_symm (x : I) : σ (σ x) = x :=
  Subtype.ext <| by simp [symm]

Involutivity of Central Symmetry on the Unit Interval

Informal description

For any element $x$ in the unit interval $I = [0,1]$, applying the central symmetry function $\sigma$ twice returns $x$, i.e., $\sigma(\sigma(x)) = x$.

unitInterval.symm_involutive theorem

: Function.Involutive (symm : I → I)

Full source

theorem symm_involutive : Function.Involutive (symm : I → I) := symm_symm

Involutivity of the Unit Interval Symmetry $\sigma$

Informal description

The central symmetry function $\sigma : [0,1] \to [0,1]$, defined by $\sigma(x) = 1 - x$, is involutive, meaning that $\sigma(\sigma(x)) = x$ for all $x \in [0,1]$.

unitInterval.symm_bijective theorem

: Function.Bijective (symm : I → I)

Full source

theorem symm_bijective : Function.Bijective (symm : I → I) := symm_involutive.bijective

Bijectivity of the Unit Interval Symmetry $\sigma(x) = 1 - x$

Informal description

The central symmetry function $\sigma : [0,1] \to [0,1]$, defined by $\sigma(x) = 1 - x$, is bijective (both injective and surjective).

unitInterval.coe_symm_eq theorem

(x : I) : (σ x : ℝ) = 1 - x

Full source

@[simp]
theorem coe_symm_eq (x : I) : (σ x : ℝ) = 1 - x :=
  rfl

Symmetry Property of the Unit Interval: $\sigma(x) = 1 - x$

Informal description

For any element $x$ in the unit interval $I = [0,1]$, the real number corresponding to its symmetric point $\sigma(x)$ is equal to $1 - x$, i.e., $\sigma(x) = 1 - x$.

unitInterval.symm_projIcc theorem

(x : ℝ) : symm (projIcc 0 1 zero_le_one x) = projIcc 0 1 zero_le_one (1 - x)

Full source

@[simp]
theorem symm_projIcc (x : ℝ) :
    symm (projIcc 0 1 zero_le_one x) = projIcc 0 1 zero_le_one (1 - x) := by
  ext
  rcases le_total x 0 with h₀ | h₀
  · simp [projIcc_of_le_left, projIcc_of_right_le, h₀]
  · rcases le_total x 1 with h₁ | h₁
    · lift x to I using ⟨h₀, h₁⟩
      simp_rw [← coe_symm_eq, projIcc_val]
    · simp [projIcc_of_le_left, projIcc_of_right_le, h₁]

Symmetry of Projection onto Unit Interval: $\sigma(\text{proj}_{[0,1]}(x)) = \text{proj}_{[0,1]}(1 - x)$

Informal description

For any real number $x$, the central symmetry $\sigma$ of the unit interval $[0,1]$ satisfies \[ \sigma(\text{projIcc}(0,1,0 \leq 1)(x)) = \text{projIcc}(0,1,0 \leq 1)(1 - x), \] where $\text{projIcc}(a,b,h)$ denotes the projection of a real number onto the closed interval $[a,b]$.

unitInterval.continuous_symm theorem

: Continuous σ

Full source

@[continuity, fun_prop]
theorem continuous_symm : Continuous σ :=
  Continuous.subtype_mk (by fun_prop) _

Continuity of Unit Interval Central Symmetry

Informal description

The central symmetry function $\sigma : [0,1] \to [0,1]$ defined by $\sigma(t) = 1 - t$ is continuous.

unitInterval.symmHomeomorph definition

: I ≃ₜ I

Full source

/-- `unitInterval.symm` as a `Homeomorph`. -/
@[simps]
def symmHomeomorph : II ≃ₜ I where
  toFun := symm
  invFun := symm
  left_inv := symm_symm
  right_inv := symm_symm

Homeomorphism of the unit interval via central symmetry

Informal description

The homeomorphism $\sigma : [0,1] \to [0,1]$ defined by $\sigma(t) = 1 - t$ is a self-homeomorphism of the unit interval, where $\sigma$ is both the forward and inverse map, and satisfies $\sigma \circ \sigma = \text{id}$.

unitInterval.strictAnti_symm theorem

: StrictAnti σ

Full source

theorem strictAnti_symm : StrictAnti σ := fun _ _ h ↦ sub_lt_sub_left (α := ℝ) h _

Strict Antitonicity of Unit Interval Central Symmetry

Informal description

The central symmetry function $\sigma : [0,1] \to [0,1]$ defined by $\sigma(t) = 1 - t$ is strictly antitone, meaning that for any $t_1, t_2 \in [0,1]$, if $t_1 < t_2$ then $\sigma(t_1) > \sigma(t_2)$.

unitInterval.symm_inj theorem

{i j : I} : σ i = σ j ↔ i = j

Full source

@[simp]
theorem symm_inj {i j : I} : σσ i = σ j ↔ i = j := symm_bijective.injective.eq_iff

Injectivity of Unit Interval Symmetry: $\sigma(i) = \sigma(j) \leftrightarrow i = j$

Informal description

For any two elements $i, j$ in the unit interval $I = [0,1]$, the central symmetry function $\sigma(t) = 1 - t$ satisfies $\sigma(i) = \sigma(j)$ if and only if $i = j$.

unitInterval.half_le_symm_iff theorem

(t : I) : 1 / 2 ≤ (σ t : ℝ) ↔ (t : ℝ) ≤ 1 / 2

Full source

theorem half_le_symm_iff (t : I) : 1 / 2 ≤ (σ t : ℝ) ↔ (t : ℝ) ≤ 1 / 2 := by
  rw [coe_symm_eq, le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le, sub_half]

Midpoint Inequality for Unit Interval Symmetry: $\frac{1}{2} \leq \sigma(t) \leftrightarrow t \leq \frac{1}{2}$

Informal description

For any element $t$ in the unit interval $I = [0,1]$, the inequality $\frac{1}{2} \leq \sigma(t)$ holds if and only if $t \leq \frac{1}{2}$, where $\sigma(t) = 1 - t$ is the central symmetry function on $I$.

unitInterval.symm_eq_one theorem

{i : I} : σ i = 1 ↔ i = 0

Full source

@[simp]
lemma symm_eq_one {i : I} : σσ i = 1 ↔ i = 0 := by
  rw [← symm_zero, symm_inj]

Central Symmetry Maps to One if and only if at Zero: $\sigma(i) = 1 \leftrightarrow i = 0$

Informal description

For any element $i$ in the unit interval $I = [0,1]$, the central symmetry function $\sigma(i) = 1 - i$ equals $1$ if and only if $i = 0$.

unitInterval.symm_eq_zero theorem

{i : I} : σ i = 0 ↔ i = 1

Full source

@[simp]
lemma symm_eq_zero {i : I} : σσ i = 0 ↔ i = 1 := by
  rw [← symm_one, symm_inj]

Central Symmetry Vanishes at One: $\sigma(i) = 0 \leftrightarrow i = 1$

Informal description

For any element $i$ in the unit interval $I = [0,1]$, the central symmetry function $\sigma(i) = 1 - i$ satisfies $\sigma(i) = 0$ if and only if $i = 1$.

unitInterval.symm_le_symm theorem

{i j : I} : σ i ≤ σ j ↔ j ≤ i

Full source

@[simp]
theorem symm_le_symm {i j : I} : σσ i ≤ σ j ↔ j ≤ i := by
  simp only [symm, Subtype.mk_le_mk, sub_le_sub_iff, add_le_add_iff_left, Subtype.coe_le_coe]

Order Reversal under Central Symmetry of the Unit Interval: $\sigma(i) \leq \sigma(j) \leftrightarrow j \leq i$

Informal description

For any two elements $i, j$ in the unit interval $[0,1]$, the inequality $\sigma(i) \leq \sigma(j)$ holds if and only if $j \leq i$, where $\sigma(t) = 1 - t$ is the central symmetry of the interval.

unitInterval.le_symm_comm theorem

{i j : I} : i ≤ σ j ↔ j ≤ σ i

Full source

theorem le_symm_comm {i j : I} : i ≤ σ j ↔ j ≤ σ i := by
  rw [← symm_le_symm, symm_symm]

Order Reversal under Central Symmetry: $i \leq \sigma(j) \leftrightarrow j \leq \sigma(i)$

Informal description

For any two elements $i, j$ in the unit interval $I = [0,1]$, the inequality $i \leq \sigma(j)$ holds if and only if $j \leq \sigma(i)$, where $\sigma(t) = 1 - t$ is the central symmetry of the interval.

unitInterval.symm_le_comm theorem

{i j : I} : σ i ≤ j ↔ σ j ≤ i

Full source

theorem symm_le_comm {i j : I} : σσ i ≤ j ↔ σ j ≤ i := by
  rw [← symm_le_symm, symm_symm]

Order Reversal under Central Symmetry: $\sigma(i) \leq j \leftrightarrow \sigma(j) \leq i$

Informal description

For any two elements $i, j$ in the unit interval $I = [0,1]$, the inequality $\sigma(i) \leq j$ holds if and only if $\sigma(j) \leq i$, where $\sigma(t) = 1 - t$ is the central symmetry of the interval.

unitInterval.symm_lt_symm theorem

{i j : I} : σ i < σ j ↔ j < i

Full source

@[simp]
theorem symm_lt_symm {i j : I} : σσ i < σ j ↔ j < i := by
  simp only [symm, Subtype.mk_lt_mk, sub_lt_sub_iff_left, Subtype.coe_lt_coe]

Order Reversal under Central Symmetry of the Unit Interval: $\sigma(i) < \sigma(j) \leftrightarrow j < i$

Informal description

For any two points $i, j$ in the unit interval $[0,1]$, the reflection $\sigma(i) = 1 - i$ is less than the reflection $\sigma(j) = 1 - j$ if and only if $j < i$.

unitInterval.lt_symm_comm theorem

{i j : I} : i < σ j ↔ j < σ i

Full source

theorem lt_symm_comm {i j : I} : i < σ j ↔ j < σ i := by
  rw [← symm_lt_symm, symm_symm]

Order Reversal under Central Symmetry: $i < \sigma(j) \leftrightarrow j < \sigma(i)$

Informal description

For any two points $i, j$ in the unit interval $I = [0,1]$, the inequality $i < \sigma(j)$ holds if and only if $j < \sigma(i)$, where $\sigma(x) = 1 - x$ is the central symmetry of the interval.

unitInterval.symm_lt_comm theorem

{i j : I} : σ i < j ↔ σ j < i

Full source

theorem symm_lt_comm {i j : I} : σσ i < j ↔ σ j < i := by
  rw [← symm_lt_symm, symm_symm]

Order Reversal under Central Symmetry: $\sigma(i) < j \leftrightarrow \sigma(j) < i$

Informal description

For any two points $i, j$ in the unit interval $I = [0,1]$, the reflection $\sigma(i) = 1 - i$ is less than $j$ if and only if the reflection $\sigma(j) = 1 - j$ is less than $i$.

unitInterval.instConnectedSpaceElemReal instance

: ConnectedSpace I

Full source

instance : ConnectedSpace I :=
  Subtype.connectedSpace ⟨nonempty_Icc.mpr zero_le_one, isPreconnected_Icc⟩

Connectedness of the Unit Interval

Informal description

The unit interval $I = [0, 1]$ in $\mathbb{R}$ is a connected topological space.

unitInterval.nonneg theorem

(x : I) : 0 ≤ (x : ℝ)

Full source

theorem nonneg (x : I) : 0 ≤ (x : ℝ) :=
  x.2.1

Nonnegativity of Elements in the Unit Interval

Informal description

For any element $x$ in the unit interval $I = [0, 1]$, the real number corresponding to $x$ is nonnegative, i.e., $0 \leq x \leq 1$.

unitInterval.one_minus_nonneg theorem

(x : I) : 0 ≤ 1 - (x : ℝ)

Full source

theorem one_minus_nonneg (x : I) : 0 ≤ 1 - (x : ℝ) := by simpa using x.2.2

Nonnegativity of One Minus Element in Unit Interval

Informal description

For any element $x$ in the unit interval $I = [0,1]$, the real number $1 - x$ is nonnegative, i.e., $0 \leq 1 - x$.

unitInterval.le_one theorem

(x : I) : (x : ℝ) ≤ 1

Full source

theorem le_one (x : I) : (x : ℝ) ≤ 1 :=
  x.2.2

Upper Bound of Unit Interval: $x \leq 1$ for $x \in [0,1]$

Informal description

For any element $x$ in the unit interval $I = [0, 1]$, the real number corresponding to $x$ satisfies $x \leq 1$.

unitInterval.one_minus_le_one theorem

(x : I) : 1 - (x : ℝ) ≤ 1

Full source

theorem one_minus_le_one (x : I) : 1 - (x : ℝ) ≤ 1 := by simpa using x.2.1

Upper Bound of One Minus Element in Unit Interval

Informal description

For any element $x$ in the unit interval $I = [0,1]$, the real number $1 - x$ satisfies $1 - x \leq 1$.

unitInterval.add_pos theorem

{t : I} {x : ℝ} (hx : 0 < x) : 0 < (x + t : ℝ)

Full source

theorem add_pos {t : I} {x : ℝ} (hx : 0 < x) : 0 < (x + t : ℝ) :=
  add_pos_of_pos_of_nonneg hx <| nonneg _

Positivity of Sum with Unit Interval Element: $0 < x + t$ for $x > 0$ and $t \in [0,1]$

Informal description

For any element $t$ in the unit interval $I = [0,1]$ and any real number $x > 0$, the sum $x + t$ is strictly positive, i.e., $0 < x + t$.

unitInterval.nonneg' theorem

{t : I} : 0 ≤ t

Full source

/-- like `unitInterval.nonneg`, but with the inequality in `I`. -/
theorem nonneg' {t : I} : 0 ≤ t :=
  t.2.1

Nonnegativity of Elements in the Unit Interval

Informal description

For any element $t$ in the unit interval $I = [0,1]$, we have $0 \leq t$.

unitInterval.le_one' theorem

{t : I} : t ≤ 1

Full source

/-- like `unitInterval.le_one`, but with the inequality in `I`. -/
theorem le_one' {t : I} : t ≤ 1 :=
  t.2.2

Upper Bound of Unit Interval Elements: $t \leq 1$ for $t \in [0,1]$

Informal description

For any element $t$ in the unit interval $I = [0,1]$, we have $t \leq 1$.

unitInterval.pos_iff_ne_zero theorem

{x : I} : 0 < x ↔ x ≠ 0

Full source

protected lemma pos_iff_ne_zero {x : I} : 0 < x ↔ x ≠ 0 := bot_lt_iff_ne_bot

Positivity Characterization in the Unit Interval: $0 < x \leftrightarrow x \neq 0$

Informal description

For any element $x$ in the unit interval $I = [0,1]$, $x$ is strictly positive if and only if $x$ is not equal to $0$, i.e., $0 < x \leftrightarrow x \neq 0$.

unitInterval.lt_one_iff_ne_one theorem

{x : I} : x < 1 ↔ x ≠ 1

Full source

protected lemma lt_one_iff_ne_one {x : I} : x < 1 ↔ x ≠ 1 := lt_top_iff_ne_top

Characterization of Strictly Less Than One in the Unit Interval: $x < 1 \leftrightarrow x \neq 1$

Informal description

For any element $x$ in the unit interval $I = [0,1]$, $x$ is strictly less than $1$ if and only if $x$ is not equal to $1$.

unitInterval.instNontrivialElemReal instance

: Nontrivial I

Full source

instance : Nontrivial I := ⟨⟨1, 0, (one_ne_zero <| congrArg Subtype.val ·)⟩⟩

Nontriviality of the Unit Interval

Informal description

The unit interval $I = [0,1]$ is a nontrivial type, meaning it contains at least two distinct elements.

unitInterval.mul_pos_mem_iff theorem

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

Full source

theorem mul_pos_mem_iff {a t : ℝ} (ha : 0 < a) : a * t ∈ Ia * t ∈ I ↔ t ∈ Set.Icc (0 : ℝ) (1 / a) := by
  constructor <;> rintro ⟨h₁, h₂⟩ <;> constructor
  · exact nonneg_of_mul_nonneg_right h₁ ha
  · rwa [le_div_iff₀ ha, mul_comm]
  · exact mul_nonneg ha.le h₁
  · rwa [le_div_iff₀ ha, mul_comm] at h₂

Membership condition for positive scalar multiplication in the unit interval: $a \cdot t \in I \leftrightarrow t \in [0, 1/a]$

Informal description

For any real numbers $a > 0$ and $t$, the product $a \cdot t$ belongs to the unit interval $I = [0, 1]$ if and only if $t$ belongs to the closed interval $\left[0, \frac{1}{a}\right]$.

unitInterval.two_mul_sub_one_mem_iff theorem

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

Full source

theorem two_mul_sub_one_mem_iff {t : ℝ} : 2 * t - 1 ∈ I2 * t - 1 ∈ I ↔ t ∈ Set.Icc (1 / 2 : ℝ) 1 := by
  constructor <;> rintro ⟨h₁, h₂⟩ <;> constructor <;> linarith

Characterization of $2t - 1$ in the Unit Interval via $t \in [\frac{1}{2}, 1]$

Informal description

For any real number $t$, the expression $2t - 1$ lies in the unit interval $I = [0,1]$ if and only if $t$ lies in the closed interval $[\frac{1}{2}, 1]$.

unitInterval.submonoid definition

: Submonoid ℝ

Full source

/-- The unit interval as a submonoid of ℝ. -/
def submonoid : Submonoid ℝ where
  carrier := unitInterval
  one_mem' := unitInterval.one_mem
  mul_mem' := unitInterval.mul_mem

Unit interval as a multiplicative submonoid of real numbers

Informal description

The unit interval $[0,1]$ forms a submonoid of the multiplicative monoid of real numbers, where the carrier set is $I = \{x \in \mathbb{R} \mid 0 \leq x \leq 1\}$, containing the multiplicative identity $1$ and closed under multiplication (i.e., for any $x, y \in I$, the product $x \cdot y$ is also in $I$).

unitInterval.coe_unitIntervalSubmonoid theorem

: submonoid = unitInterval

Full source

@[simp] theorem coe_unitIntervalSubmonoid : submonoid = unitInterval := rfl

Unit Interval Submonoid Carrier Set Equals Unit Interval

Informal description

The multiplicative submonoid structure on the unit interval $[0,1]$ has carrier set equal to $I = \{x \in \mathbb{R} \mid 0 \leq x \leq 1\}$.

unitInterval.mem_unitIntervalSubmonoid theorem

{x} : x ∈ submonoid ↔ x ∈ unitInterval

Full source

@[simp] theorem mem_unitIntervalSubmonoid {x} : x ∈ submonoidx ∈ submonoid ↔ x ∈ unitInterval :=
  Iff.rfl

Membership Criterion for Unit Interval Submonoid: $x \in \text{submonoid} \leftrightarrow x \in [0,1]$

Informal description

An element $x \in \mathbb{R}$ belongs to the multiplicative submonoid of the unit interval if and only if $x$ is in the unit interval $[0,1]$, i.e., $x \in \text{submonoid} \leftrightarrow x \in [0,1]$.

unitInterval.prod_mem theorem

 {ι : Type*} {t : Finset ι} {f : ι → ℝ} (h : ∀ c ∈ t, f c ∈ unitInterval) : ∏ c ∈ t, f c ∈ unitInterval

Full source

protected theorem prod_mem {ι : Type*} {t : Finset ι} {f : ι → ℝ}
    (h : ∀ c ∈ t, f c ∈ unitInterval) :
    ∏ c ∈ t, f c∏ c ∈ t, f c ∈ unitInterval := _root_.prod_mem (S := unitInterval.submonoid) h

Product of Unit Interval Elements Remains in Unit Interval

Informal description

For any finite index set $\iota$ and function $f : \iota \to \mathbb{R}$, if $f(c) \in [0,1]$ for every $c$ in the finite set $t \subseteq \iota$, then the product $\prod_{c \in t} f(c)$ also belongs to the unit interval $[0,1]$.

unitInterval.instLinearOrderedCommMonoidWithZeroElemReal instance

: LinearOrderedCommMonoidWithZero I

Full source

instance : LinearOrderedCommMonoidWithZero I where
  zero_mul i := zero_mul i
  mul_zero i := mul_zero i
  zero_le_one := nonneg'
  mul_le_mul_left i j h_ij k := by
    simp only [← Subtype.coe_le_coe, coe_mul]
    apply mul_le_mul le_rfl ?_ (nonneg i) (nonneg k)
    simp [h_ij]

Linearly Ordered Commutative Monoid with Zero Structure on the Unit Interval

Informal description

The unit interval $I = [0,1]$ is a linearly ordered commutative monoid with zero, where the multiplication operation is the usual multiplication of real numbers, the order is the restriction of the standard order on $\mathbb{R}$, and zero is the least element.

Set.abs_projIcc_sub_projIcc theorem

: (|projIcc a b h c - projIcc a b h d| : α) ≤ |c - d|

Full source

/-- `Set.projIcc` is a contraction. -/
lemma _root_.Set.abs_projIcc_sub_projIcc : (|projIcc a b h c - projIcc a b h d| : α) ≤ |c - d| := by
  wlog hdc : d ≤ c generalizing c d
  · rw [abs_sub_comm, abs_sub_comm c]; exact this (le_of_not_le hdc)
  rw [abs_eq_self.2 (sub_nonneg.2 hdc),
    abs_eq_self.2 (sub_nonneg.2 <| mod_cast monotone_projIcc h hdc)]
  rw [← sub_nonneg] at hdc
  refine (max_sub_max_le_max _ _ _ _).trans (max_le (by rwa [sub_self]) ?_)
  refine ((le_abs_self _).trans <| abs_min_sub_min_le_max _ _ _ _).trans (max_le ?_ ?_)
  · rwa [sub_self, abs_zero]
  · exact (abs_eq_self.mpr hdc).le

Lipschitz Continuity of Projection onto Closed Interval: $|\text{projIcc}_{a,b}(c) - \text{projIcc}_{a,b}(d)| \leq |c - d|$

Informal description

For any elements $a, b, c, d$ in a linearly ordered type $\alpha$ with $a \leq b$, the absolute difference between the projections of $c$ and $d$ onto the closed interval $[a, b]$ is bounded by the absolute difference between $c$ and $d$ themselves, i.e., \[ |\text{projIcc}_{a,b}(c) - \text{projIcc}_{a,b}(d)| \leq |c - d|. \]

Set.Icc.addNSMul definition

(δ : α) (n : ℕ) : Icc a b

Full source

/-- 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`. -/
def addNSMul (δ : α) (n : ℕ) : Icc a b := projIcc a b h (a + n • δ)

Equally spaced sequence in a closed interval with saturation at the endpoint

Informal description

Given a closed interval $[a, b]$ in a linearly ordered type $\alpha$ with $a \leq b$ (witnessed by $h$) and a positive step size $\delta$, the function $\text{addNSMul}(h, \delta, n)$ returns the point $\max(a, \min(b, a + n \cdot \delta))$ for each natural number $n$. This produces a sequence of points in $[a, b]$ that starts at $a$ and progresses in steps of size $\delta$ until reaching $b$, after which all subsequent points remain at $b$.

Set.Icc.addNSMul_zero theorem

: addNSMul h δ 0 = a

Full source

lemma addNSMul_zero : addNSMul h δ 0 = a := by
  rw [addNSMul, zero_smul, add_zero, projIcc_left]

Initial Term of Equally Spaced Sequence in Closed Interval: $\text{addNSMul}(h, \delta, 0) = a$

Informal description

For any closed interval $[a, b]$ in a linearly ordered type $\alpha$ with $a \leq b$ (witnessed by $h$) and any step size $\delta$, the first term of the equally spaced sequence generated by $\text{addNSMul}(h, \delta, \cdot)$ is equal to $a$, i.e., $\text{addNSMul}(h, \delta, 0) = a$.

Set.Icc.addNSMul_eq_right theorem

[Archimedean α] (hδ : 0 < δ) : ∃ m, ∀ n ≥ m, addNSMul h δ n = b

Full source

lemma addNSMul_eq_right [Archimedean α] (hδ : 0 < δ) :
    ∃ m, ∀ n ≥ m, addNSMul h δ n = b := by
  obtain ⟨m, hm⟩ := Archimedean.arch (b - a) hδ
  refine ⟨m, fun n hn ↦ ?_⟩
  rw [addNSMul, coe_projIcc, add_comm, min_eq_left_iff.mpr, max_eq_right h]
  exact sub_le_iff_le_add.mp (hm.trans <| nsmul_le_nsmul_left hδ.le hn)

Eventual Stabilization of Equally Spaced Sequence in Closed Interval

Informal description

Let $\alpha$ be an Archimedean linearly ordered type, and let $[a, b]$ be a closed interval in $\alpha$ with $a \leq b$. For any positive step size $\delta > 0$, there exists a natural number $m$ such that for all $n \geq m$, the $n$-th term of the sequence $\text{addNSMul}(h, \delta, n)$ equals $b$.

Set.Icc.monotone_addNSMul theorem

(hδ : 0 ≤ δ) : Monotone (addNSMul h δ)

Full source

lemma monotone_addNSMul (hδ : 0 ≤ δ) : Monotone (addNSMul h δ) :=
  fun _ _ hnm ↦ monotone_projIcc h <| (add_le_add_iff_left _).mpr (nsmul_le_nsmul_left hδ hnm)

Monotonicity of Equally Spaced Sequence in Closed Interval $[a, b]$

Informal description

For any closed interval $[a, b]$ in a linearly ordered type $\alpha$ with $a \leq b$ and a non-negative step size $\delta \geq 0$, the function $\text{addNSMul}(h, \delta, \cdot) : \mathbb{N} \to [a, b]$ is monotone. That is, for any natural numbers $n \leq m$, we have $\text{addNSMul}(h, \delta, n) \leq \text{addNSMul}(h, \delta, m)$.

Set.Icc.abs_sub_addNSMul_le theorem

 (hδ : 0 ≤ δ) {t : Icc a b} (n : ℕ) (ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))) :
  (|t - addNSMul h δ n| : α) ≤ δ

Full source

lemma abs_sub_addNSMul_le (hδ : 0 ≤ δ) {t : Icc a b} (n : ℕ)
    (ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n+1))) :
    (|t - addNSMul h δ n| : α) ≤ δ :=
  calc
    (|t - addNSMul h δ n| : α) = t - addNSMul h δ n            := abs_eq_self.2 <| sub_nonneg.2 ht.1
    _ ≤ projIcc a b h (a + (n+1) • δ) - addNSMul h δ n := by apply sub_le_sub_right; exact ht.2
    _ ≤ (|projIcc a b h (a + (n+1) • δ) - addNSMul h δ n| : α) := le_abs_self _
    _ ≤ |a + (n+1) • δ - (a + n • δ)|                          := abs_projIcc_sub_projIcc h
    _ ≤ δ := by
          rw [add_sub_add_comm, sub_self, zero_add, succ_nsmul', add_sub_cancel_right]
          exact (abs_eq_self.mpr hδ).le

Bound on Distance from Equally Spaced Points in Closed Interval: $|t - \text{addNSMul}_n| \leq \delta$

Informal description

Let $\alpha$ be a linearly ordered type, and let $[a, b]$ be a closed interval in $\alpha$ with $a \leq b$. For any non-negative step size $\delta \geq 0$, if $t$ is an element of $[a, b]$ lying between the $n$-th and $(n+1)$-th terms of the sequence $\text{addNSMul}(h, \delta, \cdot)$, then the absolute difference between $t$ and the $n$-th term is bounded by $\delta$, i.e., \[ |t - \text{addNSMul}(h, \delta, n)| \leq \delta. \]

exists_monotone_Icc_subset_open_cover_Icc theorem

 {ι} {a b : ℝ} (h : a ≤ b) {c : ι → Set (Icc a b)} (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univ ⊆ ⋃ i, c i) :
  ∃ t : ℕ → Icc a b, t 0 = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, t n = b) ∧ ∀ n, ∃ i, Icc (t n) (t (n + 1)) ⊆ c i

Full source

/-- Any open cover `c` of a closed interval `[a, b]` in ℝ
can be refined to a finite partition into subintervals. -/
lemma exists_monotone_Icc_subset_open_cover_Icc {ι} {a b : ℝ} (h : a ≤ b) {c : ι → Set (Icc a b)}
    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univuniv ⊆ ⋃ i, c i) : ∃ t : ℕ → Icc a b, t 0 = a ∧
      Monotone t ∧ (∃ m, ∀ n ≥ m, t n = b) ∧ ∀ n, ∃ i, Icc (t n) (t (n + 1)) ⊆ c i := by
  obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
  have hδ := half_pos δ_pos
  refine ⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n ↦ ?_⟩
  obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ/2) n) trivial
  exact ⟨i, fun t ht ↦ hsub ((abs_sub_addNSMul_le h hδ.le n ht).trans_lt <| half_lt_self δ_pos)⟩

Existence of Monotone Partition for Open Cover of Closed Interval in $\mathbb{R}$

Informal description

Let $[a, b]$ be a closed interval in $\mathbb{R}$ with $a \leq b$, and let $\{c_i\}_{i \in \iota}$ be an open cover of $[a, b]$. Then there exists a monotone sequence $(t_n)_{n \in \mathbb{N}}$ in $[a, b]$ such that: 1. $t_0 = a$, 2. $(t_n)$ is monotone increasing, 3. There exists $m \in \mathbb{N}$ such that $t_n = b$ for all $n \geq m$, 4. For each $n$, there exists $i \in \iota$ such that the subinterval $[t_n, t_{n+1}]$ is contained in $c_i$.

exists_monotone_Icc_subset_open_cover_unitInterval theorem

 {ι} {c : ι → Set I} (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univ ⊆ ⋃ i, c i) :
  ∃ t : ℕ → I, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ n, ∃ i, Icc (t n) (t (n + 1)) ⊆ c i

Full source

/-- Any open cover of the unit interval can be refined to a finite partition into subintervals. -/
lemma exists_monotone_Icc_subset_open_cover_unitInterval {ι} {c : ι → Set I}
    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univuniv ⊆ ⋃ i, c i) : ∃ t : ℕ → I, t 0 = 0 ∧
      Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ n, ∃ i, Icc (t n) (t (n + 1)) ⊆ c i := by
  simp_rw [← Subtype.coe_inj]
  exact exists_monotone_Icc_subset_open_cover_Icc zero_le_one hc₁ hc₂

Existence of Monotone Partition for Open Covers of the Unit Interval

Informal description

Let $I = [0,1]$ be the unit interval in $\mathbb{R}$. For any open cover $\{c_i\}_{i \in \iota}$ of $I$ (where each $c_i$ is an open subset of $I$), there exists a monotone sequence $(t_n)_{n \in \mathbb{N}}$ in $I$ such that: 1. $t_0 = 0$, 2. $(t_n)$ is monotone increasing, 3. There exists $N \in \mathbb{N}$ such that $t_n = 1$ for all $n \geq N$, 4. For each $n$, there exists $i \in \iota$ such that the subinterval $[t_n, t_{n+1}]$ is contained in $c_i$.

exists_monotone_Icc_subset_open_cover_unitInterval_prod_self theorem

 {ι} {c : ι → Set (I × I)} (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univ ⊆ ⋃ i, c i) :
  ∃ t : ℕ → I,
    t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ n m, ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i

Full source

lemma exists_monotone_Icc_subset_open_cover_unitInterval_prod_self {ι} {c : ι → Set (II × I)}
    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univuniv ⊆ ⋃ i, c i) :
    ∃ t : ℕ → I, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧
      ∀ n m, ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i := by
  obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
  have hδ := half_pos δ_pos
  simp_rw [Subtype.ext_iff]
  have h : (0 : ℝ) ≤ 1 := zero_le_one
  refine ⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n m ↦ ?_⟩
  obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ/2) n, addNSMul h (δ/2) m) trivial
  exact ⟨i, fun t ht ↦ hsub (Metric.mem_ball.mpr <| (max_le (abs_sub_addNSMul_le h hδ.le n ht.1) <|
    abs_sub_addNSMul_le h hδ.le m ht.2).trans_lt <| half_lt_self δ_pos)⟩

Existence of Monotone Partition for Open Covers of Unit Square $I \times I$

Informal description

Let $I = [0,1]$ be the unit interval in $\mathbb{R}$. For any open cover $\{c_i\}_{i \in \iota}$ of $I \times I$ (where each $c_i$ is an open subset of $I \times I$), there exists a monotone sequence $(t_n)_{n \in \mathbb{N}}$ in $I$ such that: 1. $t_0 = 0$, 2. $(t_n)$ is monotone increasing, 3. There exists $N$ such that $t_n = 1$ for all $n \geq N$, 4. For every $n, m \in \mathbb{N}$, there exists $i \in \iota$ such that the product of intervals $[t_n, t_{n+1}] \times [t_m, t_{m+1}]$ is contained in $c_i$.

projIcc_eq_zero theorem

{x : ℝ} : projIcc (0 : ℝ) 1 zero_le_one x = 0 ↔ x ≤ 0

Full source

@[simp]
theorem projIcc_eq_zero {x : ℝ} : projIccprojIcc (0 : ℝ) 1 zero_le_one x = 0 ↔ x ≤ 0 :=
  projIcc_eq_left zero_lt_one

Projection onto Unit Interval Equals Zero iff $x \leq 0$

Informal description

For any real number $x$, the projection of $x$ onto the closed unit interval $[0, 1]$ equals $0$ if and only if $x \leq 0$.

projIcc_eq_one theorem

{x : ℝ} : projIcc (0 : ℝ) 1 zero_le_one x = 1 ↔ 1 ≤ x

Full source

@[simp]
theorem projIcc_eq_one {x : ℝ} : projIccprojIcc (0 : ℝ) 1 zero_le_one x = 1 ↔ 1 ≤ x :=
  projIcc_eq_right zero_lt_one

Projection onto Unit Interval Equals One iff $x \geq 1$

Informal description

For any real number $x$, the projection of $x$ onto the closed unit interval $[0,1]$ equals $1$ if and only if $x \geq 1$.

Tactic.Interactive.tacticUnit_interval definition

: Lean.ParserDescr✝

Full source

macromacro "unit_interval" : tactic =>
  `(tactic| (first
  | apply unitInterval.nonneg
  | apply unitInterval.one_minus_nonneg
  | apply unitInterval.le_one
  | apply unitInterval.one_minus_le_one))

Unit interval inequalities tactic

Informal description

A tactic that automatically proves the inequalities $0 \leq x$, $0 \leq 1 - x$, $x \leq 1$, and $1 - x \leq 1$ for any $x$ in the unit interval $I = [0,1] \subset \mathbb{R}$.

affineHomeomorph_image_I theorem

(a b : 𝕜) (h : 0 < a) : affineHomeomorph a b h.ne.symm '' Set.Icc 0 1 = Set.Icc b (a + b)

Full source

/-- The image of `[0,1]` under the homeomorphism `fun x ↦ a * x + b` is `[b, a+b]`.
-/
theorem affineHomeomorph_image_I (a b : 𝕜) (h : 0 < a) :
    affineHomeomorphaffineHomeomorph a b h.ne.symm '' Set.Icc 0 1 = Set.Icc b (a + b) := by simp [h]

Image of Unit Interval under Affine Homeomorphism with Positive Slope

Informal description

Let $\mathbb{K}$ be a topological field, and let $a, b \in \mathbb{K}$ with $a > 0$. The image of the closed unit interval $[0, 1]$ under the affine homeomorphism $x \mapsto a x + b$ is the closed interval $[b, a + b]$. That is, $$ \{a x + b \mid x \in [0, 1]\} = [b, a + b]. $$

iccHomeoI definition

(a b : 𝕜) (h : a < b) : Set.Icc a b ≃ₜ Set.Icc (0 : 𝕜) (1 : 𝕜)

Full source

/-- The affine homeomorphism from a nontrivial interval `[a,b]` to `[0,1]`.
-/
def iccHomeoI (a b : 𝕜) (h : a < b) : Set.IccSet.Icc a b ≃ₜ Set.Icc (0 : 𝕜) (1 : 𝕜) := by
  let e := Homeomorph.image (affineHomeomorph (b - a) a (sub_pos.mpr h).ne.symm) (Set.Icc 0 1)
  refine (e.trans ?_).symm
  apply Homeomorph.setCongr
  rw [affineHomeomorph_image_I _ _ (sub_pos.2 h)]
  simp

Homeomorphism between $[a,b]$ and $[0,1]$

Informal description

For a topological field $\mathbb{K}$ and elements $a, b \in \mathbb{K}$ with $a < b$, the function $x \mapsto \frac{x - a}{b - a}$ defines a homeomorphism between the closed intervals $[a, b]$ and $[0, 1]$. The inverse homeomorphism is given by $y \mapsto (b - a)y + a$.

iccHomeoI_apply_coe theorem

(a b : 𝕜) (h : a < b) (x : Set.Icc a b) : ((iccHomeoI a b h) x : 𝕜) = (x - a) / (b - a)

Full source

@[simp]
theorem iccHomeoI_apply_coe (a b : 𝕜) (h : a < b) (x : Set.Icc a b) :
    ((iccHomeoI a b h) x : 𝕜) = (x - a) / (b - a) :=
  rfl

Image of Point under Homeomorphism from $[a,b]$ to $[0,1]$

Informal description

For any elements $a, b$ in a topological field $\mathbb{K}$ with $a < b$, and for any $x$ in the closed interval $[a, b]$, the image of $x$ under the homeomorphism $\text{iccHomeoI}$ is given by $\frac{x - a}{b - a}$.

iccHomeoI_symm_apply_coe theorem

(a b : 𝕜) (h : a < b) (x : Set.Icc (0 : 𝕜) (1 : 𝕜)) : ((iccHomeoI a b h).symm x : 𝕜) = (b - a) * x + a

Full source

@[simp]
theorem iccHomeoI_symm_apply_coe (a b : 𝕜) (h : a < b) (x : Set.Icc (0 : 𝕜) (1 : 𝕜)) :
    ((iccHomeoI a b h).symm x : 𝕜) = (b - a) * x + a :=
  rfl

Inverse Homeomorphism Formula for $[a,b] \leftrightarrow [0,1]$

Informal description

For a topological field $\mathbb{K}$ and elements $a, b \in \mathbb{K}$ with $a < b$, the inverse of the homeomorphism between $[a, b]$ and $[0, 1]$ is given by the formula $y \mapsto (b - a)y + a$ for any $y \in [0, 1]$. Specifically, for any $x \in [0, 1]$, the image under the inverse homeomorphism is $(b - a)x + a$ as an element of $\mathbb{K}$.

unitInterval.toNNReal definition

: I → ℝ≥0

Full source

/-- The coercion from `I` to `ℝ≥0`. -/
def unitInterval.toNNReal : I → ℝ≥0 := fun i ↦ ⟨i.1, i.2.1⟩

Inclusion of the unit interval into nonnegative reals

Informal description

The function maps an element $x$ of the unit interval $I = [0,1]$ to the corresponding nonnegative real number in $\mathbb{R}_{\geq 0}$, where the value is simply the underlying real number of $x$ (which is guaranteed to be nonnegative since $x \in I$).

unitInterval.toNNReal_continuous theorem

: Continuous toNNReal

Full source

@[fun_prop]
lemma unitInterval.toNNReal_continuous : Continuous toNNReal := by
  delta toNNReal
  fun_prop

Continuity of the Unit Interval Inclusion into Nonnegative Reals

Informal description

The inclusion map from the unit interval $I = [0,1]$ to the nonnegative real numbers $\mathbb{R}_{\geq 0}$ is continuous.

unitInterval.coe_toNNReal theorem

(x : I) : ((toNNReal x) : ℝ) = x

Full source

@[simp]
lemma unitInterval.coe_toNNReal (x : I) : ((toNNReal x) : ℝ) = x := rfl

Inclusion of Unit Interval into Nonnegative Reals Preserves Value

Informal description

For any element $x$ in the unit interval $I = [0,1]$, the underlying real number of the nonnegative real number obtained by applying the inclusion map $\mathrm{toNNReal}$ to $x$ is equal to $x$ itself. That is, $\mathrm{toNNReal}(x) = x$ as real numbers.