doc-next-gen

Mathlib.Topology.Path

Module docstring

{"# Paths in topological spaces

This file introduces continuous paths and provides API for them.

Main definitions

In this file the unit interval [0, 1] in ℝ is denoted by I, and X is a topological space.

  • Path x y is the type of paths from x to y, i.e., continuous maps from I to X mapping 0 to x and 1 to y.
  • Path.refl x : Path x x is the constant path at x.
  • Path.symm γ : Path y x is the reverse of a path γ : Path x y.
  • Path.trans γ γ' : Path x z is the concatenation of two paths γ : Path x y, γ' : Path y z.
  • Path.map γ hf : Path (f x) (f y) is the image of γ : Path x y under a continuous map f.
  • Path.reparam γ f hf hf₀ hf₁ : Path x y is the reparametrisation of γ : Path x y by a continuous map f : I → I fixing 0 and 1.
  • Path.truncate γ t₀ t₁ : Path (γ t₀) (γ t₁) is the path that follows γ from t₀ to t₁ and stays constant otherwise.
  • Path.extend γ : ℝ → X is the extension γ to ℝ that is constant before 0 and after 1.

Path x y is equipped with the topology induced by the compact-open topology on C(I,X), and several of the above constructions are shown to be continuous.

Implementation notes

By default, all paths have I as their source and X as their target, but there is an operation Set.IccExtend that will extend any continuous map γ : I → X into a continuous map IccExtend zero_le_one γ : ℝ → X that is constant before 0 and after 1.

This is used to define Path.extend that turns γ : Path x y into a continuous map γ.extend : ℝ → X whose restriction to I is the original γ, and is equal to x on (-∞, 0] and to y on [1, +∞). ","### Paths ","#### Space of paths ","#### Product of paths ","#### Pointwise multiplication/addition of two paths in a topological (additive) group ","#### Truncating a path ","#### Reparametrising a path "}

Path structure
(x y : X) extends C(I, X)
Full source 
/-- Continuous path connecting two points `x` and `y` in a topological space -/
structure Path (x y : X) extends C(I, X) where
  /-- The start point of a `Path`. -/
  source' : toFun 0 = x
  /-- The end point of a `Path`. -/
  target' : toFun 1 = y
Continuous path in a topological space
Informal description
A continuous path from point $x$ to point $y$ in a topological space $X$ is a continuous function $\gamma : [0,1] \to X$ such that $\gamma(0) = x$ and $\gamma(1) = y$.
Path.funLike instance
: FunLike (Path x y) I X
Full source 
instance Path.funLike : FunLike (Path x y) I X where
  coe γ := ⇑γ.toContinuousMap
  coe_injective' γ₁ γ₂ h := by
    simp only [DFunLike.coe_fn_eq] at h
    cases γ₁; cases γ₂; congr
Function-Like Structure on Paths
Informal description
For any topological space $X$ and points $x, y \in X$, the type of continuous paths from $x$ to $y$ (i.e., continuous functions $\gamma: [0,1] \to X$ with $\gamma(0) = x$ and $\gamma(1) = y$) can be treated as a function-like type, where each path $\gamma$ can be coerced to a function from the unit interval $I = [0,1]$ to $X$.
Path.continuousMapClass instance
: ContinuousMapClass (Path x y) I X
Full source 
instance Path.continuousMapClass : ContinuousMapClass (Path x y) I X where
  map_continuous γ := show Continuous γ.toContinuousMap by fun_prop
Continuous Paths as Continuous Maps
Informal description
For any topological space $X$ and points $x, y \in X$, the type of continuous paths from $x$ to $y$ is equipped with the structure of continuous maps from the unit interval $I = [0,1]$ to $X$. This means that every path $\gamma : \text{Path}\,x\,y$ can be treated as a continuous function $\gamma : I \to X$ with $\gamma(0) = x$ and $\gamma(1) = y$.
Path.ext theorem
: ∀ {γ₁ γ₂ : Path x y}, (γ₁ : I → X) = γ₂ → γ₁ = γ₂
Full source 
@[ext]
protected theorem Path.ext : ∀ {γ₁ γ₂ : Path x y}, (γ₁ : I → X) = γ₂ → γ₁ = γ₂ := by
  rintro ⟨⟨x, h11⟩, h12, h13⟩ ⟨⟨x, h21⟩, h22, h23⟩ rfl
  rfl
Extensionality of Paths in Topological Spaces
Informal description
For any two paths $\gamma_1, \gamma_2$ from $x$ to $y$ in a topological space $X$, if the underlying continuous functions $\gamma_1, \gamma_2 : [0,1] \to X$ are equal, then $\gamma_1 = \gamma_2$.
Path.coe_mk_mk theorem
(f : I → X) (h₁) (h₂ : f 0 = x) (h₃ : f 1 = y) : ⇑(mk ⟨f, h₁⟩ h₂ h₃ : Path x y) = f
Full source 
@[simp]
theorem coe_mk_mk (f : I → X) (h₁) (h₂ : f 0 = x) (h₃ : f 1 = y) :
    ⇑(mk ⟨f, h₁⟩ h₂ h₃ : Path x y) = f :=
  rfl
Path Construction Preserves Underlying Function
Informal description
For any continuous function $f : [0,1] \to X$ with $f(0) = x$ and $f(1) = y$, the coercion of the path constructed from $f$ (with proofs of continuity and endpoint conditions) is equal to $f$ itself. In other words, if $\gamma$ is the path defined by $\gamma(t) = f(t)$ for $t \in [0,1]$, then $\gamma = f$ as functions.
Path.continuous theorem
: Continuous γ
Full source 
@[continuity]
protected theorem continuous : Continuous γ :=
  γ.continuous_toFun
Continuity of Paths in Topological Spaces
Informal description
For any path $\gamma$ from $x$ to $y$ in a topological space $X$, the function $\gamma : [0,1] \to X$ is continuous.
Path.source theorem
: γ 0 = x
Full source 
@[simp]
protected theorem source : γ 0 = x :=
  γ.source'
Path Starting Point Property
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the starting point of $\gamma$ is $x$, i.e., $\gamma(0) = x$.
Path.target theorem
: γ 1 = y
Full source 
@[simp]
protected theorem target : γ 1 = y :=
  γ.target'
Path Endpoint Property: $\gamma(1) = y$
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the endpoint of $\gamma$ at $1$ is equal to $y$, i.e., $\gamma(1) = y$.
Path.simps.apply definition
: I → X
Full source 
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections. -/
def simps.apply : I → X :=
  γ
Path application function
Informal description
The function application of a path $\gamma$ from $x$ to $y$ in a topological space $X$ is the underlying continuous function $\gamma : [0,1] \to X$.
Path.coe_toContinuousMap theorem
: ⇑γ.toContinuousMap = γ
Full source 
@[simp]
theorem coe_toContinuousMap : ⇑γ.toContinuousMap = γ :=
  rfl
Equality of Path and its Continuous Map Representation
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the underlying continuous map $\gamma_{\text{cont}}$ associated with $\gamma$ is equal to $\gamma$ when viewed as a function from the unit interval $I = [0,1]$ to $X$. In other words, $\gamma_{\text{cont}}(t) = \gamma(t)$ for all $t \in [0,1]$.
Path.coe_mk theorem
: ⇑(γ : C(I, X)) = γ
Full source 
@[simp]
theorem coe_mk : ⇑(γ : C(I, X)) = γ :=
  rfl
Path as Continuous Map Preserves Function Application
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, when viewed as a continuous map $\gamma \in C(I,X)$, its underlying function is equal to $\gamma$ itself. That is, $\gamma(t) = \gamma(t)$ for all $t \in [0,1]$.
Path.hasUncurryPath instance
{X α : Type*} [TopologicalSpace X] {x y : α → X} : HasUncurry (∀ a : α, Path (x a) (y a)) (α × I) X
Full source 
/-- Any function `φ : Π (a : α), Path (x a) (y a)` can be seen as a function `α × I → X`. -/
instance hasUncurryPath {X α : Type*} [TopologicalSpace X] {x y : α → X} :
    HasUncurry (∀ a : α, Path (x a) (y a)) (α × I) X :=
  ⟨fun φ p => φ p.1 p.2⟩
Uncurrying of Path Families
Informal description
For any topological space $X$, index type $\alpha$, and functions $x, y : \alpha \to X$, a family of paths $\gamma_a : [0,1] \to X$ from $x(a)$ to $y(a)$ for each $a \in \alpha$ can be viewed as a single continuous function $\gamma : \alpha \times [0,1] \to X$ defined by $\gamma(a,t) = \gamma_a(t)$.
Path.refl definition
(x : X) : Path x x
Full source 
/-- The constant path from a point to itself -/
@[refl, simps]
def refl (x : X) : Path x x where
  toFun _t := x
  continuous_toFun := continuous_const
  source' := rfl
  target' := rfl
Constant path
Informal description
The constant path at a point $x$ in a topological space $X$ is the continuous function $\gamma : [0,1] \to X$ defined by $\gamma(t) = x$ for all $t \in [0,1]$, with $\gamma(0) = x$ and $\gamma(1) = x$.
Path.refl_range theorem
{a : X} : range (Path.refl a) = { a }
Full source 
@[simp]
theorem refl_range {a : X} : range (Path.refl a) = {a} := by simp [Path.refl, CoeFun.coe]
Range of Constant Path is Singleton Set
Informal description
For any point $a$ in a topological space $X$, the range of the constant path $\gamma(t) = a$ for all $t \in [0,1]$ is the singleton set $\{a\}$.
Path.symm definition
(γ : Path x y) : Path y x
Full source 
/-- The reverse of a path from `x` to `y`, as a path from `y` to `x` -/
@[symm, simps]
def symm (γ : Path x y) : Path y x where
  toFun := γ ∘ σ
  continuous_toFun := by fun_prop
  source' := by simp
  target' := by simp
Reverse of a continuous path
Informal description
Given a continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the reverse path $\gamma^{-1}$ is defined as the continuous function from $[0,1]$ to $X$ given by $\gamma^{-1}(t) = \gamma(1-t)$. This path goes from $y$ to $x$, with $\gamma^{-1}(0) = y$ and $\gamma^{-1}(1) = x$.
Path.symm_symm theorem
(γ : Path x y) : γ.symm.symm = γ
Full source 
@[simp]
theorem symm_symm (γ : Path x y) : γ.symm.symm = γ := by
  ext t
  show γ (σ (σ t)) = γ t
  rw [unitInterval.symm_symm]
Double Reverse of a Path Equals Original Path
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the double reverse of $\gamma$ equals $\gamma$ itself, i.e., $(\gamma^{-1})^{-1} = \gamma$.
Path.symm_bijective theorem
: Function.Bijective (Path.symm : Path x y → Path y x)
Full source 
theorem symm_bijective : Function.Bijective (Path.symm : Path x y → Path y x) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
Bijectivity of Path Reversal Operation
Informal description
The path reversal operation $\gamma \mapsto \gamma^{-1}$, which maps a continuous path $\gamma : [0,1] \to X$ from $x$ to $y$ to its reverse path $\gamma^{-1}(t) = \gamma(1-t)$ from $y$ to $x$, is a bijective function between the space of paths from $x$ to $y$ and the space of paths from $y$ to $x$.
Path.refl_symm theorem
{a : X} : (Path.refl a).symm = Path.refl a
Full source 
@[simp]
theorem refl_symm {a : X} : (Path.refl a).symm = Path.refl a := by
  ext
  rfl
Reverse of Constant Path Equals Itself
Informal description
For any point $a$ in a topological space $X$, the reverse of the constant path at $a$ is equal to the constant path at $a$ itself, i.e., $(\text{refl}_a)^{-1} = \text{refl}_a$.
Path.symm_range theorem
{a b : X} (γ : Path a b) : range γ.symm = range γ
Full source 
@[simp]
theorem symm_range {a b : X} (γ : Path a b) : range γ.symm = range γ :=
  symm_involutive.surjective.range_comp γ
Range Preservation under Path Reversal
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, the range of the reverse path $\gamma^{-1}$ is equal to the range of $\gamma$, i.e., $\text{range}(\gamma^{-1}) = \text{range}(\gamma)$.
Path.topologicalSpace instance
: TopologicalSpace (Path x y)
Full source 
/-- The following instance defines the topology on the path space to be induced from the
compact-open topology on the space `C(I,X)` of continuous maps from `I` to `X`.
-/
instance topologicalSpace : TopologicalSpace (Path x y) :=
  TopologicalSpace.induced ((↑) : _ → C(I, X)) ContinuousMap.compactOpen
Topology on the Space of Continuous Paths
Informal description
The space of continuous paths from $x$ to $y$ in a topological space $X$ is equipped with the topology induced by the compact-open topology on the space of continuous maps from the unit interval $I = [0,1]$ to $X$.
Path.instContinuousEvalElemRealUnitInterval instance
: ContinuousEval (Path x y) I X
Full source 
instance : ContinuousEval (Path x y) I X := .of_continuous_forget continuous_induced_dom
Continuity of Path Evaluation
Informal description
For any topological space $X$ and points $x, y \in X$, the evaluation map $(γ, t) \mapsto γ(t)$ is continuous, where $γ$ is a path from $x$ to $y$ (i.e., a continuous function $γ : [0,1] \to X$ with $γ(0) = x$ and $γ(1) = y$) and $t \in [0,1]$.
Path.continuous_uncurry_iff theorem
{Y} [TopologicalSpace Y] {g : Y → Path x y} : Continuous ↿g ↔ Continuous g
Full source 
theorem continuous_uncurry_iff {Y} [TopologicalSpace Y] {g : Y → Path x y} :
    ContinuousContinuous ↿g ↔ Continuous g :=
  Iff.symm <| continuous_induced_rng.trans
    ⟨fun h => continuous_uncurry_of_continuous ⟨_, h⟩,
    continuous_of_continuous_uncurry (fun (y : Y) ↦ ContinuousMap.mk (g y))⟩
Equivalence of Continuity for Path-Valued Functions and Their Uncurried Forms
Informal description
For any topological space $Y$ and a function $g : Y \to \text{Path}\,x\,y$ mapping elements of $Y$ to continuous paths from $x$ to $y$ in $X$, the uncurried function $\text{↿}g : Y \times [0,1] \to X$ defined by $\text{↿}g(y,t) = g(y)(t)$ is continuous if and only if $g$ is continuous.
Path.extend definition
: ℝ → X
Full source 
/-- A continuous map extending a path to `ℝ`, constant before `0` and after `1`. -/
def extend : ℝ → X :=
  IccExtend zero_le_one γ
Extension of a path to the real line
Informal description
The extension of a continuous path $\gamma : [0,1] \to X$ to a continuous function $\gamma_{\text{ext}} : \mathbb{R} \to X$ that is constant on $(-\infty, 0]$ and $[1, \infty)$, with $\gamma_{\text{ext}}(t) = \gamma(0)$ for $t \leq 0$ and $\gamma_{\text{ext}}(t) = \gamma(1)$ for $t \geq 1$, and $\gamma_{\text{ext}}(t) = \gamma(t)$ for $t \in [0,1]$.
Continuous.path_extend theorem
{γ : Y → Path x y} {f : Y → ℝ} (hγ : Continuous ↿γ) (hf : Continuous f) : Continuous fun t => (γ t).extend (f t)
Full source 
/-- See Note [continuity lemma statement]. -/
theorem _root_.Continuous.path_extend {γ : Y → Path x y} {f : Y → ℝ} (hγ : Continuous ↿γ)
    (hf : Continuous f) : Continuous fun t => (γ t).extend (f t) :=
  Continuous.IccExtend hγ hf
Continuity of Path Extension under Continuous Evaluation
Informal description
Let $Y$ be a topological space, and let $\gamma \colon Y \to \text{Path}\,x\,y$ be a continuous family of paths from $x$ to $y$ in a topological space $X$, where the uncurried function $\gamma \colon Y \times [0,1] \to X$ is continuous. If $f \colon Y \to \mathbb{R}$ is a continuous function, then the extended path evaluation function $t \mapsto (\gamma(t)).\text{extend}(f(t))$ is continuous.
Path.continuous_extend theorem
: Continuous γ.extend
Full source 
/-- A useful special case of `Continuous.path_extend`. -/
@[continuity, fun_prop]
theorem continuous_extend : Continuous γ.extend :=
  γ.continuous.Icc_extend'
Continuity of Path Extension to Real Line
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the extended function $\gamma_{\text{ext}} : \mathbb{R} \to X$ is continuous. Here $\gamma_{\text{ext}}$ is defined to be constant on $(-\infty, 0]$ and $[1, \infty)$, with $\gamma_{\text{ext}}(t) = \gamma(0)$ for $t \leq 0$ and $\gamma_{\text{ext}}(t) = \gamma(1)$ for $t \geq 1$, and agrees with $\gamma$ on $[0,1]$.
Filter.Tendsto.path_extend theorem
{l r : Y → X} {y : Y} {l₁ : Filter ℝ} {l₂ : Filter X} {γ : ∀ y, Path (l y) (r y)} (hγ : Tendsto (↿γ) (𝓝 y ×ˢ l₁.map (projIcc 0 1 zero_le_one)) l₂) : Tendsto (↿fun x => (γ x).extend) (𝓝 y ×ˢ l₁) l₂
Full source 
theorem _root_.Filter.Tendsto.path_extend
    {l r : Y → X} {y : Y} {l₁ : Filter ℝ} {l₂ : Filter X} {γ : ∀ y, Path (l y) (r y)}
    (hγ : Tendsto (↿γ) (𝓝 y ×ˢ l₁.map (projIcc 0 1 zero_le_one)) l₂) :
    Tendsto (↿fun x => (γ x).extend) (𝓝 y ×ˢ l₁) l₂ :=
  Filter.Tendsto.IccExtend _ hγ
Limit Behavior of Extended Path Families
Informal description
Let $Y$ be a topological space, $X$ a topological space, and for each $y \in Y$, let $\gamma_y$ be a continuous path from $l(y)$ to $r(y)$ in $X$. Let $y \in Y$ be a point, and let $l_1$ be a filter on $\mathbb{R}$ and $l_2$ a filter on $X$. If the uncurried path family $\gamma : Y \times [0,1] \to X$ tends to $l_2$ along the product filter of the neighborhood filter $\mathcal{N}(y)$ and the pushforward of $l_1$ under the projection $\text{projIcc}(0,1,0 \leq 1)$, then the extended path family $\gamma_{\text{ext}} : Y \times \mathbb{R} \to X$, defined by $\gamma_{\text{ext}}(x,t) = (\gamma_x).\text{extend}(t)$, tends to $l_2$ along the product filter of $\mathcal{N}(y)$ and $l_1$.
ContinuousAt.path_extend theorem
{g : Y → ℝ} {l r : Y → X} (γ : ∀ y, Path (l y) (r y)) {y : Y} (hγ : ContinuousAt (↿γ) (y, projIcc 0 1 zero_le_one (g y))) (hg : ContinuousAt g y) : ContinuousAt (fun i => (γ i).extend (g i)) y
Full source 
theorem _root_.ContinuousAt.path_extend {g : Y → ℝ} {l r : Y → X} (γ : ∀ y, Path (l y) (r y))
    {y : Y} (hγ : ContinuousAt (↿γ) (y, projIcc 0 1 zero_le_one (g y))) (hg : ContinuousAt g y) :
    ContinuousAt (fun i => (γ i).extend (g i)) y :=
  hγ.IccExtend (fun x => γ x) hg
Continuity of Extended Path Family at a Point
Informal description
Let $Y$ be a topological space, $X$ a topological space, and for each $y \in Y$, let $\gamma_y$ be a continuous path from $l(y)$ to $r(y)$ in $X$. Given a function $g : Y \to \mathbb{R}$ and a point $y \in Y$, if the uncurried path family $\gamma : Y \times [0,1] \to X$ is continuous at $(y, \text{projIcc}(0,1,0 \leq 1)(g(y)))$ and $g$ is continuous at $y$, then the extended path function $i \mapsto (\gamma_i).\text{extend}(g(i))$ is continuous at $y$.
Path.extend_extends theorem
{a b : X} (γ : Path a b) {t : ℝ} (ht : t ∈ (Icc 0 1 : Set ℝ)) : γ.extend t = γ ⟨t, ht⟩
Full source 
@[simp]
theorem extend_extends {a b : X} (γ : Path a b) {t : ℝ}
    (ht : t ∈ (Icc 0 1 : Set ℝ)) : γ.extend t = γ ⟨t, ht⟩ :=
  IccExtend_of_mem _ γ ht
Path Extension Preserves Values on $[0,1]$
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, and for any real number $t$ in the closed interval $[0,1]$, the extension $\gamma_{\text{ext}}$ of $\gamma$ to $\mathbb{R}$ satisfies $\gamma_{\text{ext}}(t) = \gamma(t)$.
Path.extend_zero theorem
: γ.extend 0 = x
Full source 
theorem extend_zero : γ.extend 0 = x := by simp
Path Extension at Zero: $\gamma_{\text{ext}}(0) = x$
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the extension $\gamma_{\text{ext}}$ of $\gamma$ to $\mathbb{R}$ satisfies $\gamma_{\text{ext}}(0) = x$.
Path.extend_one theorem
: γ.extend 1 = y
Full source 
theorem extend_one : γ.extend 1 = y := by simp
Path Extension at Endpoint: $\gamma_{\text{ext}}(1) = y$
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the extension $\gamma_{\text{ext}}$ of $\gamma$ to $\mathbb{R}$ satisfies $\gamma_{\text{ext}}(1) = y$.
Path.extend_extends' theorem
{a b : X} (γ : Path a b) (t : (Icc 0 1 : Set ℝ)) : γ.extend t = γ t
Full source 
theorem extend_extends' {a b : X} (γ : Path a b) (t : (Icc 0 1 : Set ℝ)) : γ.extend t = γ t :=
  IccExtend_val _ γ t
Path Extension Preserves Values on $[0,1]$
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, and for any $t$ in the closed interval $[0,1]$, the extension $\gamma_{\text{ext}}$ of $\gamma$ to $\mathbb{R}$ satisfies $\gamma_{\text{ext}}(t) = \gamma(t)$.
Path.extend_range theorem
{a b : X} (γ : Path a b) : range γ.extend = range γ
Full source 
@[simp]
theorem extend_range {a b : X} (γ : Path a b) :
    range γ.extend = range γ :=
  IccExtend_range _ γ
Range Equality for Path Extension
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, the range of the extended path $\gamma_{\text{ext}} : \mathbb{R} \to X$ is equal to the range of the original path $\gamma : [0,1] \to X$. That is, \[ \text{range}(\gamma_{\text{ext}}) = \text{range}(\gamma). \]
Path.extend_of_le_zero theorem
{a b : X} (γ : Path a b) {t : ℝ} (ht : t ≤ 0) : γ.extend t = a
Full source 
theorem extend_of_le_zero {a b : X} (γ : Path a b) {t : ℝ}
    (ht : t ≤ 0) : γ.extend t = a :=
  (IccExtend_of_le_left _ _ ht).trans γ.source
Extension of Path is Constant Before Zero: $\gamma_{\text{ext}}(t) = a$ for $t \leq 0$
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, and for any real number $t \leq 0$, the extension $\gamma_{\text{ext}}$ of $\gamma$ to $\mathbb{R}$ satisfies $\gamma_{\text{ext}}(t) = a$.
Path.extend_of_one_le theorem
{a b : X} (γ : Path a b) {t : ℝ} (ht : 1 ≤ t) : γ.extend t = b
Full source 
theorem extend_of_one_le {a b : X} (γ : Path a b) {t : ℝ}
    (ht : 1 ≤ t) : γ.extend t = b :=
  (IccExtend_of_right_le _ _ ht).trans γ.target
Extension of Path Beyond Unit Interval: $\gamma_{\text{ext}}(t) = b$ for $t \geq 1$
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, and for any real number $t \geq 1$, the extended path $\gamma_{\text{ext}}$ satisfies $\gamma_{\text{ext}}(t) = b$.
Path.refl_extend theorem
{a : X} : (Path.refl a).extend = fun _ => a
Full source 
@[simp]
theorem refl_extend {a : X} : (Path.refl a).extend = fun _ => a :=
  rfl
Extension of Constant Path is Constant Function
Informal description
For any point $a$ in a topological space $X$, the extension of the constant path at $a$ to the real line is the constant function that maps every real number to $a$, i.e., $(\text{refl } a)_{\text{ext}}(t) = a$ for all $t \in \mathbb{R}$.
Path.extend_symm_apply theorem
(γ : Path x y) (t : ℝ) : γ.symm.extend t = γ.extend (1 - t)
Full source 
theorem extend_symm_apply (γ : Path x y) (t : ℝ) : γ.symm.extend t = γ.extend (1 - t) :=
  congrArg γ <| symm_projIcc _
Extension of Reverse Path Equals Original Path Evaluated at $1-t$
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the extension of the reverse path $\gamma^{-1}$ at any real number $t$ equals the extension of $\gamma$ at $1-t$, i.e., $\gamma^{-1}_{\text{ext}}(t) = \gamma_{\text{ext}}(1-t)$.
Path.extend_symm theorem
(γ : Path x y) : γ.symm.extend = (γ.extend <| 1 - ·)
Full source 
@[simp]
theorem extend_symm (γ : Path x y) : γ.symm.extend = (γ.extend <| 1 - ·) :=
  funext γ.extend_symm_apply
Extension of Reverse Path Equals Original Path Evaluated at $1-t$
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the extension of the reverse path $\gamma^{-1}$ to the real line satisfies $\gamma^{-1}_{\text{ext}}(t) = \gamma_{\text{ext}}(1 - t)$ for all $t \in \mathbb{R}$.
Path.ofLine definition
{f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y) : Path x y
Full source 
/-- The path obtained from a map defined on `ℝ` by restriction to the unit interval. -/
def ofLine {f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y) : Path x y where
  toFun := f ∘ ((↑) : unitInterval → ℝ)
  continuous_toFun := hf.comp_continuous continuous_subtype_val Subtype.prop
  source' := h₀
  target' := h₁
Path obtained by restricting a continuous function to the unit interval
Informal description
Given a continuous function $f \colon \mathbb{R} \to X$ restricted to the unit interval $I = [0,1]$, with $f(0) = x$ and $f(1) = y$, the function `Path.ofLine` constructs a continuous path $\gamma \colon I \to X$ from $x$ to $y$ by restricting $f$ to $I$. The resulting path $\gamma$ satisfies $\gamma(t) = f(t)$ for all $t \in I$.
Path.ofLine_mem theorem
{f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y) : ∀ t, ofLine hf h₀ h₁ t ∈ f '' I
Full source 
theorem ofLine_mem {f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y) :
    ∀ t, ofLineofLine hf h₀ h₁ t ∈ f '' I := fun ⟨t, t_in⟩ => ⟨t, t_in, rfl⟩
Image Membership Property for Paths Constructed from Continuous Functions
Informal description
For any continuous function $f \colon \mathbb{R} \to X$ restricted to the unit interval $I = [0,1]$, with $f(0) = x$ and $f(1) = y$, the path $\gamma = \text{ofLine}\, hf\, h₀\, h₁$ satisfies $\gamma(t) \in f(I)$ for all $t \in I$, where $f(I)$ denotes the image of $I$ under $f$.
Path.ofLine_extend theorem
(γ : Path x y) : ofLine (by fun_prop) (extend_zero γ) (extend_one γ) = γ
Full source 
@[simp]
theorem ofLine_extend (γ : Path x y) : ofLine (by fun_prop) (extend_zero γ) (extend_one γ) = γ := by
  ext t
  simp [ofLine]
Restriction of Path Extension Recovers Original Path
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the path obtained by restricting the extended function $\gamma_{\text{ext}} : \mathbb{R} \to X$ to the unit interval $[0,1]$ is equal to $\gamma$ itself. Here $\gamma_{\text{ext}}$ is defined to be constant on $(-\infty, 0]$ and $[1, \infty)$, with $\gamma_{\text{ext}}(t) = x$ for $t \leq 0$ and $\gamma_{\text{ext}}(t) = y$ for $t \geq 1$, and $\gamma_{\text{ext}}(t) = \gamma(t)$ for $t \in [0,1]$.
Path.trans definition
(γ : Path x y) (γ' : Path y z) : Path x z
Full source 
/-- Concatenation of two paths from `x` to `y` and from `y` to `z`, putting the first
path on `[0, 1/2]` and the second one on `[1/2, 1]`. -/
@[trans]
def trans (γ : Path x y) (γ' : Path y z) : Path x z where
  toFun := (fun t : ℝ => if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ (↑)
  continuous_toFun := by
    refine
      (Continuous.if_le ?_ ?_ continuous_id continuous_const (by norm_num)).comp
        continuous_subtype_val <;>
    fun_prop
  source' := by norm_num
  target' := by norm_num
Concatenation of paths in a topological space
Informal description
Given two continuous paths $\gamma \colon [0,1] \to X$ from $x$ to $y$ and $\gamma' \colon [0,1] \to X$ from $y$ to $z$ in a topological space $X$, their concatenation $\gamma \cdot \gamma' \colon [0,1] \to X$ is defined as the path that follows $\gamma$ at double speed on $[0, \frac{1}{2}]$ and $\gamma'$ at double speed (shifted by $-1$) on $[\frac{1}{2}, 1]$, resulting in a continuous path from $x$ to $z$.
Path.trans_apply theorem
(γ : Path x y) (γ' : Path y z) (t : I) : (γ.trans γ') t = if h : (t : ℝ) ≤ 1 / 2 then γ ⟨2 * t, (mul_pos_mem_iff zero_lt_two).2 ⟨t.2.1, h⟩⟩ else γ' ⟨2 * t - 1, two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, t.2.2⟩⟩
Full source 
theorem trans_apply (γ : Path x y) (γ' : Path y z) (t : I) :
    (γ.trans γ') t =
      if h : (t : ℝ) ≤ 1 / 2 then γ ⟨2 * t, (mul_pos_mem_iff zero_lt_two).2 ⟨t.2.1, h⟩⟩
      else γ' ⟨2 * t - 1, two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, t.2.2⟩⟩ :=
  show ite _ _ _ = _ by split_ifs <;> rw [extend_extends]
Evaluation Formula for Concatenated Paths
Informal description
Let $\gamma \colon [0,1] \to X$ be a continuous path from $x$ to $y$ and $\gamma' \colon [0,1] \to X$ be a continuous path from $y$ to $z$ in a topological space $X$. For any $t \in [0,1]$, the concatenated path $\gamma \cdot \gamma'$ evaluated at $t$ is given by: \[ (\gamma \cdot \gamma')(t) = \begin{cases} \gamma(2t) & \text{if } t \leq \frac{1}{2}, \\ \gamma'(2t - 1) & \text{if } t > \frac{1}{2}. \end{cases} \]
Path.trans_symm theorem
(γ : Path x y) (γ' : Path y z) : (γ.trans γ').symm = γ'.symm.trans γ.symm
Full source 
@[simp]
theorem trans_symm (γ : Path x y) (γ' : Path y z) : (γ.trans γ').symm = γ'.symm.trans γ.symm := by
  ext t
  simp only [trans_apply, ← one_div, symm_apply, not_le, Function.comp_apply]
  split_ifs with h h₁ h₂ <;> rw [coe_symm_eq] at h
  · have ht : (t : ℝ) = 1 / 2 := by linarith
    norm_num [ht]
  · refine congr_arg _ (Subtype.ext ?_)
    norm_num [sub_sub_eq_add_sub, mul_sub]
  · refine congr_arg _ (Subtype.ext ?_)
    norm_num [mul_sub, h]
    ring -- TODO norm_num should really do this
  · exfalso
    linarith
Reverse of Concatenated Path Equals Concatenation of Reversed Paths
Informal description
For any continuous paths $\gamma$ from $x$ to $y$ and $\gamma'$ from $y$ to $z$ in a topological space $X$, the reverse of the concatenated path $\gamma \cdot \gamma'$ is equal to the concatenation of the reversed paths $\gamma'^{-1} \cdot \gamma^{-1}$.
Path.refl_trans_refl theorem
{a : X} : (Path.refl a).trans (Path.refl a) = Path.refl a
Full source 
@[simp]
theorem refl_trans_refl {a : X} :
    (Path.refl a).trans (Path.refl a) = Path.refl a := by
  ext
  simp only [Path.trans, ite_self, one_div, Path.refl_extend]
  rfl
Concatenation of Constant Paths Yields Constant Path
Informal description
For any point $a$ in a topological space $X$, the concatenation of the constant path at $a$ with itself is equal to the constant path at $a$.
Path.trans_range theorem
{a b c : X} (γ₁ : Path a b) (γ₂ : Path b c) : range (γ₁.trans γ₂) = range γ₁ ∪ range γ₂
Full source 
theorem trans_range {a b c : X} (γ₁ : Path a b) (γ₂ : Path b c) :
    range (γ₁.trans γ₂) = rangerange γ₁ ∪ range γ₂ := by
  rw [Path.trans]
  apply eq_of_subset_of_subset
  · rintro x ⟨⟨t, ht0, ht1⟩, hxt⟩
    by_cases h : t ≤ 1 / 2
    · left
      use ⟨2 * t, ⟨by linarith, by linarith⟩⟩
      rw [← γ₁.extend_extends]
      rwa [coe_mk_mk, Function.comp_apply, if_pos h] at hxt
    · right
      use ⟨2 * t - 1, ⟨by linarith, by linarith⟩⟩
      rw [← γ₂.extend_extends]
      rwa [coe_mk_mk, Function.comp_apply, if_neg h] at hxt
  · rintro x (⟨⟨t, ht0, ht1⟩, hxt⟩ | ⟨⟨t, ht0, ht1⟩, hxt⟩)
    · use ⟨t / 2, ⟨by linarith, by linarith⟩⟩
      have : t / 2 ≤ 1 / 2 := (div_le_div_iff_of_pos_right (zero_lt_two : (0 : ℝ) < 2)).mpr ht1
      rw [coe_mk_mk, Function.comp_apply, if_pos this, Subtype.coe_mk]
      ring_nf
      rwa [γ₁.extend_extends]
    · by_cases h : t = 0
      · use ⟨1 / 2, ⟨by linarith, by linarith⟩⟩
        rw [coe_mk_mk, Function.comp_apply, if_pos le_rfl, Subtype.coe_mk,
          mul_one_div_cancel (two_ne_zero' ℝ)]
        rw [γ₁.extend_one]
        rwa [← γ₂.extend_extends, h, γ₂.extend_zero] at hxt
      · use ⟨(t + 1) / 2, ⟨by linarith, by linarith⟩⟩
        replace h : t ≠ 0 := h
        have ht0 := lt_of_le_of_ne ht0 h.symm
        have : ¬(t + 1) / 2 ≤ 1 / 2 := by
          rw [not_le]
          linarith
        rw [coe_mk_mk, Function.comp_apply, Subtype.coe_mk, if_neg this]
        ring_nf
        rwa [γ₂.extend_extends]
Range of Concatenated Path Equals Union of Ranges
Informal description
For any points $a, b, c$ in a topological space $X$ and continuous paths $\gamma_1$ from $a$ to $b$ and $\gamma_2$ from $b$ to $c$, the range of the concatenated path $\gamma_1 \cdot \gamma_2$ is equal to the union of the ranges of $\gamma_1$ and $\gamma_2$, i.e., $\text{range}(\gamma_1 \cdot \gamma_2) = \text{range}(\gamma_1) \cup \text{range}(\gamma_2)$.
Path.map' definition
(γ : Path x y) {f : X → Y} (h : ContinuousOn f (range γ)) : Path (f x) (f y)
Full source 
/-- Image of a path from `x` to `y` by a map which is continuous on the path. -/
def map' (γ : Path x y) {f : X → Y} (h : ContinuousOn f (range γ)) : Path (f x) (f y) where
  toFun := f ∘ γ
  continuous_toFun := h.comp_continuous γ.continuous (fun x ↦ mem_range_self x)
  source' := by simp
  target' := by simp
Image of a path under a continuous function
Informal description
Given a continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, and a function $f: X \to Y$ that is continuous on the range of $\gamma$, the image of $\gamma$ under $f$ is a continuous path from $f(x)$ to $f(y)$ in $Y$.
Path.map definition
(γ : Path x y) {f : X → Y} (h : Continuous f) : Path (f x) (f y)
Full source 
/-- Image of a path from `x` to `y` by a continuous map -/
def map (γ : Path x y) {f : X → Y} (h : Continuous f) :
    Path (f x) (f y) := γ.map' h.continuousOn
Image of a path under a continuous map
Informal description
Given a continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, and a continuous function $f: X \to Y$, the image of $\gamma$ under $f$ is a continuous path from $f(x)$ to $f(y)$ in $Y$.
Path.map_coe theorem
(γ : Path x y) {f : X → Y} (h : Continuous f) : (γ.map h : I → Y) = f ∘ γ
Full source 
@[simp]
theorem map_coe (γ : Path x y) {f : X → Y} (h : Continuous f) :
    (γ.map h : I → Y) = f ∘ γ := by
  ext t
  rfl
Function Representation of Path Image: $(\gamma \circ f) = f \circ \gamma$
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, and any continuous function $f: X \to Y$, the function representation of the mapped path $\gamma \circ f$ is equal to the composition $f \circ \gamma$ when viewed as functions from the unit interval $I = [0,1]$ to $Y$.
Path.map_symm theorem
(γ : Path x y) {f : X → Y} (h : Continuous f) : (γ.map h).symm = γ.symm.map h
Full source 
@[simp]
theorem map_symm (γ : Path x y) {f : X → Y} (h : Continuous f) :
    (γ.map h).symm = γ.symm.map h :=
  rfl
Commutativity of Path Reversal and Continuous Mapping: $(f \circ \gamma)^{-1} = f \circ \gamma^{-1}$
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, and any continuous function $f: X \to Y$, the reverse of the image of $\gamma$ under $f$ is equal to the image of the reverse path $\gamma^{-1}$ under $f$. That is, $(f \circ \gamma)^{-1} = f \circ \gamma^{-1}$.
Path.map_trans theorem
(γ : Path x y) (γ' : Path y z) {f : X → Y} (h : Continuous f) : (γ.trans γ').map h = (γ.map h).trans (γ'.map h)
Full source 
@[simp]
theorem map_trans (γ : Path x y) (γ' : Path y z) {f : X → Y}
    (h : Continuous f) : (γ.trans γ').map h = (γ.map h).trans (γ'.map h) := by
  ext t
  rw [trans_apply, map_coe, Function.comp_apply, trans_apply]
  split_ifs <;> rfl
Image of Concatenated Paths Equals Concatenation of Images: $f \circ (\gamma \cdot \gamma') = (f \circ \gamma) \cdot (f \circ \gamma')$
Informal description
Let $X$ and $Y$ be topological spaces, and let $\gamma \colon [0,1] \to X$ be a continuous path from $x$ to $y$ and $\gamma' \colon [0,1] \to X$ be a continuous path from $y$ to $z$. For any continuous function $f \colon X \to Y$, the image of the concatenated path $\gamma \cdot \gamma'$ under $f$ is equal to the concatenation of the images of $\gamma$ and $\gamma'$ under $f$, i.e., \[ f \circ (\gamma \cdot \gamma') = (f \circ \gamma) \cdot (f \circ \gamma'). \]
Path.map_id theorem
(γ : Path x y) : γ.map continuous_id = γ
Full source 
@[simp]
theorem map_id (γ : Path x y) : γ.map continuous_id = γ := by
  ext
  rfl
Identity Mapping Preserves Paths
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the image of $\gamma$ under the identity map is equal to $\gamma$ itself, i.e., $\gamma \circ \text{id} = \gamma$.
Path.map_map theorem
(γ : Path x y) {Z : Type*} [TopologicalSpace Z] {f : X → Y} (hf : Continuous f) {g : Y → Z} (hg : Continuous g) : (γ.map hf).map hg = γ.map (hg.comp hf)
Full source 
@[simp]
theorem map_map (γ : Path x y) {Z : Type*} [TopologicalSpace Z]
    {f : X → Y} (hf : Continuous f) {g : Y → Z} (hg : Continuous g) :
    (γ.map hf).map hg = γ.map (hg.comp hf) := by
  ext
  rfl
Composition of Path Mappings via Function Composition
Informal description
Let $X$, $Y$, and $Z$ be topological spaces, and let $\gamma$ be a continuous path from $x$ to $y$ in $X$. For any continuous functions $f: X \to Y$ and $g: Y \to Z$, the composition of path mappings satisfies $(\gamma \circ f) \circ g = \gamma \circ (g \circ f)$, where $\circ$ denotes the path mapping operation.
Path.cast definition
(γ : Path x y) {x' y'} (hx : x' = x) (hy : y' = y) : Path x' y'
Full source 
/-- Casting a path from `x` to `y` to a path from `x'` to `y'` when `x' = x` and `y' = y` -/
def cast (γ : Path x y) {x' y'} (hx : x' = x) (hy : y' = y) : Path x' y' where
  toFun := γ
  continuous_toFun := γ.continuous
  source' := by simp [hx]
  target' := by simp [hy]
Relabeling of path endpoints
Informal description
Given a continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, and given points $x'$ and $y'$ such that $x' = x$ and $y' = y$, the function returns a path from $x'$ to $y'$ that is identical to $\gamma$ but with the endpoints relabeled.
Path.symm_cast theorem
{a₁ a₂ b₁ b₂ : X} (γ : Path a₂ b₂) (ha : a₁ = a₂) (hb : b₁ = b₂) : (γ.cast ha hb).symm = γ.symm.cast hb ha
Full source 
@[simp]
theorem symm_cast {a₁ a₂ b₁ b₂ : X} (γ : Path a₂ b₂) (ha : a₁ = a₂) (hb : b₁ = b₂) :
    (γ.cast ha hb).symm = γ.symm.cast hb ha :=
  rfl
Commutativity of Path Reversal and Endpoint Relabeling
Informal description
Let $X$ be a topological space and let $\gamma$ be a continuous path from $a_2$ to $b_2$ in $X$. Given points $a_1, a_2, b_1, b_2 \in X$ such that $a_1 = a_2$ and $b_1 = b_2$, the reverse of the relabeled path $\gamma.\text{cast}(ha, hb)$ is equal to the relabeled reverse path $\gamma.\text{symm}.\text{cast}(hb, ha)$. In other words, $(\gamma.\text{cast}(ha, hb))^{-1} = \gamma^{-1}.\text{cast}(hb, ha)$.
Path.trans_cast theorem
{a₁ a₂ b₁ b₂ c₁ c₂ : X} (γ : Path a₂ b₂) (γ' : Path b₂ c₂) (ha : a₁ = a₂) (hb : b₁ = b₂) (hc : c₁ = c₂) : (γ.cast ha hb).trans (γ'.cast hb hc) = (γ.trans γ').cast ha hc
Full source 
@[simp]
theorem trans_cast {a₁ a₂ b₁ b₂ c₁ c₂ : X} (γ : Path a₂ b₂)
    (γ' : Path b₂ c₂) (ha : a₁ = a₂) (hb : b₁ = b₂) (hc : c₁ = c₂) :
    (γ.cast ha hb).trans (γ'.cast hb hc) = (γ.trans γ').cast ha hc :=
  rfl
Compatibility of Path Concatenation with Endpoint Relabeling
Informal description
Let $X$ be a topological space and let $\gamma \colon [0,1] \to X$ be a continuous path from $a_2$ to $b_2$, and $\gamma' \colon [0,1] \to X$ a continuous path from $b_2$ to $c_2$. Given points $a_1, b_1, c_1 \in X$ such that $a_1 = a_2$, $b_1 = b_2$, and $c_1 = c_2$, the concatenation of the relabeled paths $\gamma.\text{cast}(ha, hb)$ and $\gamma'.\text{cast}(hb, hc)$ is equal to the relabeled concatenation $(\gamma \cdot \gamma').\text{cast}(ha, hc)$, where $ha$, $hb$, and $hc$ are the respective equality proofs.
Path.cast_coe theorem
(γ : Path x y) {x' y'} (hx : x' = x) (hy : y' = y) : (γ.cast hx hy : I → X) = γ
Full source 
@[simp]
theorem cast_coe (γ : Path x y) {x' y'} (hx : x' = x) (hy : y' = y) : (γ.cast hx hy : I → X) = γ :=
  rfl
Endpoint Relabeling Preserves Path Function: $\gamma.\mathrm{cast}\, hx\, hy = \gamma$
Informal description
Given a continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, and given points $x'$ and $y'$ such that $x' = x$ and $y' = y$, the function obtained by relabeling the endpoints of $\gamma$ (denoted $\gamma.\mathrm{cast}\, hx\, hy$) is equal to $\gamma$ when both are viewed as functions from the unit interval $I = [0,1]$ to $X$.
Path.symm_continuous_family theorem
{ι : Type*} [TopologicalSpace ι] {a b : ι → X} (γ : ∀ t : ι, Path (a t) (b t)) (h : Continuous ↿γ) : Continuous ↿fun t => (γ t).symm
Full source 
@[continuity, fun_prop]
theorem symm_continuous_family {ι : Type*} [TopologicalSpace ι]
    {a b : ι → X} (γ : ∀ t : ι, Path (a t) (b t)) (h : Continuous ↿γ) :
    Continuous ↿fun t => (γ t).symm :=
  h.comp (continuous_id.prodMap continuous_symm)
Continuity of Family of Reversed Paths
Informal description
Let $X$ be a topological space, $\iota$ a topological space, and $a, b \colon \iota \to X$ continuous functions. Given a family of continuous paths $\gamma_t \colon [0,1] \to X$ from $a(t)$ to $b(t)$ for each $t \in \iota$, if the uncurried function $\tilde{\gamma} \colon \iota \times [0,1] \to X$ defined by $\tilde{\gamma}(t,s) = \gamma_t(s)$ is continuous, then the family of reversed paths $(\gamma_t)^{-1} \colon [0,1] \to X$ from $b(t)$ to $a(t)$ also has a continuous uncurried version $\tilde{\gamma}^{-1} \colon \iota \times [0,1] \to X$ defined by $\tilde{\gamma}^{-1}(t,s) = \gamma_t(1-s)$.
Path.continuous_symm theorem
: Continuous (symm : Path x y → Path y x)
Full source 
@[continuity]
theorem continuous_symm : Continuous (symm : Path x y → Path y x) :=
  continuous_uncurry_iff.mp <| symm_continuous_family _ (by fun_prop)
Continuity of Path Reversal Operation
Informal description
The path reversal operation $\text{symm} : \text{Path}\,x\,y \to \text{Path}\,y\,x$, which sends a continuous path $\gamma$ from $x$ to $y$ to its reverse $\gamma^{-1}$ (defined by $\gamma^{-1}(t) = \gamma(1-t)$), is continuous with respect to the compact-open topology on the space of paths.
Path.continuous_uncurry_extend_of_continuous_family theorem
{ι : Type*} [TopologicalSpace ι] {a b : ι → X} (γ : ∀ t : ι, Path (a t) (b t)) (h : Continuous ↿γ) : Continuous ↿fun t => (γ t).extend
Full source 
@[continuity]
theorem continuous_uncurry_extend_of_continuous_family {ι : Type*} [TopologicalSpace ι]
    {a b : ι → X} (γ : ∀ t : ι, Path (a t) (b t)) (h : Continuous ↿γ) :
    Continuous ↿fun t => (γ t).extend := by
  apply h.comp (continuous_id.prodMap continuous_projIcc)
  exact zero_le_one
Continuity of Family of Extended Paths
Informal description
Let $X$ be a topological space, $\iota$ a topological space, and $a, b \colon \iota \to X$ continuous functions. Given a family of continuous paths $\gamma_t \colon [0,1] \to X$ from $a(t)$ to $b(t)$ for each $t \in \iota$, if the uncurried function $\tilde{\gamma} \colon \iota \times [0,1] \to X$ defined by $\tilde{\gamma}(t,s) = \gamma_t(s)$ is continuous, then the family of extended paths $\gamma_t^{\text{ext}} \colon \mathbb{R} \to X$ (which are constant outside $[0,1]$ and equal to $\gamma_t$ on $[0,1]$) also has a continuous uncurried version $\tilde{\gamma}^{\text{ext}} \colon \iota \times \mathbb{R} \to X$ defined by $\tilde{\gamma}^{\text{ext}}(t,r) = \gamma_t^{\text{ext}}(r)$.
Path.trans_continuous_family theorem
{ι : Type*} [TopologicalSpace ι] {a b c : ι → X} (γ₁ : ∀ t : ι, Path (a t) (b t)) (h₁ : Continuous ↿γ₁) (γ₂ : ∀ t : ι, Path (b t) (c t)) (h₂ : Continuous ↿γ₂) : Continuous ↿fun t => (γ₁ t).trans (γ₂ t)
Full source 
@[continuity]
theorem trans_continuous_family {ι : Type*} [TopologicalSpace ι]
    {a b c : ι → X} (γ₁ : ∀ t : ι, Path (a t) (b t)) (h₁ : Continuous ↿γ₁)
    (γ₂ : ∀ t : ι, Path (b t) (c t)) (h₂ : Continuous ↿γ₂) :
    Continuous ↿fun t => (γ₁ t).trans (γ₂ t) := by
  have h₁' := Path.continuous_uncurry_extend_of_continuous_family γ₁ h₁
  have h₂' := Path.continuous_uncurry_extend_of_continuous_family γ₂ h₂
  simp only [HasUncurry.uncurry, CoeFun.coe, Path.trans, (· ∘ ·)]
  refine Continuous.if_le ?_ ?_ (continuous_subtype_val.comp continuous_snd) continuous_const ?_
  · change
      Continuous ((fun p : ι × ℝ => (γ₁ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x : I → ℝ))
    exact h₁'.comp (continuous_id.prodMap <| continuous_const.mul continuous_subtype_val)
  · change
      Continuous ((fun p : ι × ℝ => (γ₂ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x - 1 : I → ℝ))
    exact
      h₂'.comp
        (continuous_id.prodMap <|
          (continuous_const.mul continuous_subtype_val).sub continuous_const)
  · rintro st hst
    simp [hst, mul_inv_cancel₀ (two_ne_zero' ℝ)]
Continuity of Concatenated Path Families in Topological Spaces
Informal description
Let $X$ be a topological space, $\iota$ a topological space, and $a, b, c \colon \iota \to X$ continuous functions. Given two families of continuous paths $\gamma_{1,t} \colon [0,1] \to X$ from $a(t)$ to $b(t)$ and $\gamma_{2,t} \colon [0,1] \to X$ from $b(t)$ to $c(t)$ for each $t \in \iota$, if the uncurried functions $\tilde{\gamma}_1 \colon \iota \times [0,1] \to X$ and $\tilde{\gamma}_2 \colon \iota \times [0,1] \to X$ defined by $\tilde{\gamma}_1(t,s) = \gamma_{1,t}(s)$ and $\tilde{\gamma}_2(t,s) = \gamma_{2,t}(s)$ are continuous, then the family of concatenated paths $(\gamma_{1,t} \cdot \gamma_{2,t}) \colon [0,1] \to X$ from $a(t)$ to $c(t)$ also has a continuous uncurried version $\tilde{\gamma} \colon \iota \times [0,1] \to X$ defined by $\tilde{\gamma}(t,s) = (\gamma_{1,t} \cdot \gamma_{2,t})(s)$.
Continuous.path_trans theorem
{f : Y → Path x y} {g : Y → Path y z} : Continuous f → Continuous g → Continuous fun t => (f t).trans (g t)
Full source 
@[continuity, fun_prop]
theorem _root_.Continuous.path_trans {f : Y → Path x y} {g : Y → Path y z} :
    Continuous f → Continuous g → Continuous fun t => (f t).trans (g t) := by
  intro hf hg
  apply continuous_uncurry_iff.mp
  exact trans_continuous_family _ (continuous_uncurry_iff.mpr hf) _ (continuous_uncurry_iff.mpr hg)
Continuity of Path Concatenation for Continuous Path-Valued Functions
Informal description
Let $Y$ be a topological space and $X$ another topological space with points $x, y, z \in X$. Given two continuous functions $f \colon Y \to \text{Path}\,x\,y$ and $g \colon Y \to \text{Path}\,y\,z$, the function $h \colon Y \to \text{Path}\,x\,z$ defined by $h(t) = f(t) \cdot g(t)$ (the concatenation of paths $f(t)$ and $g(t)$) is also continuous.
Path.continuous_trans theorem
{x y z : X} : Continuous fun ρ : Path x y × Path y z => ρ.1.trans ρ.2
Full source 
@[continuity, fun_prop]
theorem continuous_trans {x y z : X} : Continuous fun ρ : PathPath x y × Path y z => ρ.1.trans ρ.2 := by
  fun_prop
Continuity of Path Concatenation Operation
Informal description
For any points $x, y, z$ in a topological space $X$, the concatenation operation $\text{trans} \colon \text{Path}\,x\,y \times \text{Path}\,y\,z \to \text{Path}\,x\,z$ is continuous, where $\text{Path}\,a\,b$ denotes the space of continuous paths from $a$ to $b$ in $X$.
Path.prod definition
(γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : Path (a₁, b₁) (a₂, b₂)
Full source 
/-- Given a path in `X` and a path in `Y`, we can take their pointwise product to get a path in
`X × Y`. -/
protected def prod (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : Path (a₁, b₁) (a₂, b₂) where
  toContinuousMap := ContinuousMap.prodMk γ₁.toContinuousMap γ₂.toContinuousMap
  source' := by simp
  target' := by simp
Product of paths in topological spaces
Informal description
Given two paths $\gamma_1 : [0,1] \to X$ from $a_1$ to $a_2$ and $\gamma_2 : [0,1] \to Y$ from $b_1$ to $b_2$, their product $\gamma_1 \times \gamma_2$ is the path in $X \times Y$ defined by $t \mapsto (\gamma_1(t), \gamma_2(t))$, which connects $(a_1, b_1)$ to $(a_2, b_2)$.
Path.prod_coe theorem
(γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : ⇑(γ₁.prod γ₂) = fun t => (γ₁ t, γ₂ t)
Full source 
@[simp]
theorem prod_coe (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) :
    ⇑(γ₁.prod γ₂) = fun t => (γ₁ t, γ₂ t) :=
  rfl
Coefficient Formula for Product of Paths: $(\gamma_1 \times \gamma_2)(t) = (\gamma_1(t), \gamma_2(t))$
Informal description
For any two paths $\gamma_1 : [0,1] \to X$ from $a_1$ to $a_2$ and $\gamma_2 : [0,1] \to Y$ from $b_1$ to $b_2$, the product path $\gamma_1 \times \gamma_2 : [0,1] \to X \times Y$ satisfies $(\gamma_1 \times \gamma_2)(t) = (\gamma_1(t), \gamma_2(t))$ for all $t \in [0,1]$.
Path.trans_prod_eq_prod_trans theorem
(γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂) (δ₂ : Path b₂ b₃) : (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)
Full source 
/-- Path composition commutes with products -/
theorem trans_prod_eq_prod_trans (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂)
    (δ₂ : Path b₂ b₃) : (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂) := by
  ext t <;>
  unfold Path.trans <;>
  simp only [Path.coe_mk_mk, Path.prod_coe, Function.comp_apply] <;>
  split_ifs <;>
  rfl
Commutativity of Path Concatenation with Products: $(\gamma_1 \times \gamma_2) \cdot (\delta_1 \times \delta_2) = (\gamma_1 \cdot \delta_1) \times (\gamma_2 \cdot \delta_2)$
Informal description
For any paths $\gamma_1$ from $a_1$ to $a_2$, $\delta_1$ from $a_2$ to $a_3$ in space $X$, and $\gamma_2$ from $b_1$ to $b_2$, $\delta_2$ from $b_2$ to $b_3$ in space $Y$, the concatenation of the product paths $\gamma_1 \times \gamma_2$ and $\delta_1 \times \delta_2$ equals the product of the concatenated paths $(\gamma_1 \cdot \delta_1) \times (\gamma_2 \cdot \delta_2)$. In other words: $$(\gamma_1 \times \gamma_2) \cdot (\delta_1 \times \delta_2) = (\gamma_1 \cdot \delta_1) \times (\gamma_2 \cdot \delta_2)$$
Path.pi definition
(γ : ∀ i, Path (as i) (bs i)) : Path as bs
Full source 
/-- Given a family of paths, one in each Xᵢ, we take their pointwise product to get a path in
Π i, Xᵢ. -/
protected def pi (γ : ∀ i, Path (as i) (bs i)) : Path as bs where
  toContinuousMap := ContinuousMap.pi fun i => (γ i).toContinuousMap
  source' := by simp
  target' := by simp
Product of paths in a family of topological spaces
Informal description
Given a family of paths $\gamma_i : [0,1] \to X_i$ for each $i$ in some index set, with $\gamma_i(0) = a_i$ and $\gamma_i(1) = b_i$, the product path $\gamma : [0,1] \to \prod_i X_i$ is defined by $\gamma(t) = (\gamma_i(t))_{i}$ for all $t \in [0,1]$, with $\gamma(0) = (a_i)_i$ and $\gamma(1) = (b_i)_i$.
Path.pi_coe theorem
(γ : ∀ i, Path (as i) (bs i)) : ⇑(Path.pi γ) = fun t i => γ i t
Full source 
@[simp]
theorem pi_coe (γ : ∀ i, Path (as i) (bs i)) : ⇑(Path.pi γ) = fun t i => γ i t :=
  rfl
Explicit Formula for Product Path Evaluation
Informal description
For a family of paths $\gamma_i : [0,1] \to X_i$ with $\gamma_i(0) = a_i$ and $\gamma_i(1) = b_i$ for each index $i$, the product path $\gamma = \text{Path.pi } \gamma$ satisfies $\gamma(t) = (\gamma_i(t))_{i}$ for all $t \in [0,1]$.
Path.trans_pi_eq_pi_trans theorem
(γ₀ : ∀ i, Path (as i) (bs i)) (γ₁ : ∀ i, Path (bs i) (cs i)) : (Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun i => (γ₀ i).trans (γ₁ i)
Full source 
/-- Path composition commutes with products -/
theorem trans_pi_eq_pi_trans (γ₀ : ∀ i, Path (as i) (bs i)) (γ₁ : ∀ i, Path (bs i) (cs i)) :
    (Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun i => (γ₀ i).trans (γ₁ i) := by
  ext t i
  unfold Path.trans
  simp only [Path.coe_mk_mk, Function.comp_apply, pi_coe]
  split_ifs <;> rfl
Concatenation of Product Paths Equals Product of Concatenated Paths
Informal description
Let $X_i$ be a family of topological spaces indexed by $i$, and for each $i$, let $\gamma_{0,i} \colon [0,1] \to X_i$ be a continuous path from $a_i$ to $b_i$ and $\gamma_{1,i} \colon [0,1] \to X_i$ be a continuous path from $b_i$ to $c_i$. Then the concatenation of the product paths $\prod_i \gamma_{0,i}$ and $\prod_i \gamma_{1,i}$ is equal to the product of the concatenated paths $\prod_i (\gamma_{0,i} \cdot \gamma_{1,i})$, where $\cdot$ denotes path concatenation. In other words, $(\prod_i \gamma_{0,i}) \cdot (\prod_i \gamma_{1,i}) = \prod_i (\gamma_{0,i} \cdot \gamma_{1,i})$.
Path.mul definition
[Mul X] [ContinuousMul X] {a₁ b₁ a₂ b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) : Path (a₁ * a₂) (b₁ * b₂)
Full source 
/-- Pointwise multiplication of paths in a topological group. The additive version is probably more
useful. -/
@[to_additive "Pointwise addition of paths in a topological additive group."]
protected def mul [Mul X] [ContinuousMul X] {a₁ b₁ a₂ b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) :
    Path (a₁ * a₂) (b₁ * b₂) :=
  (γ₁.prod γ₂).map continuous_mul
Pointwise product of paths in a topological group
Informal description
Given a topological space $X$ equipped with a continuous multiplication operation, and two paths $\gamma_1 : [0,1] \to X$ from $a_1$ to $b_1$ and $\gamma_2 : [0,1] \to X$ from $a_2$ to $b_2$, their pointwise product $\gamma_1 \cdot \gamma_2$ is the path from $a_1 \cdot a_2$ to $b_1 \cdot b_2$ defined by $t \mapsto \gamma_1(t) \cdot \gamma_2(t)$ for all $t \in [0,1]$.
Path.mul_apply theorem
[Mul X] [ContinuousMul X] {a₁ b₁ a₂ b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) (t : unitInterval) : (γ₁.mul γ₂) t = γ₁ t * γ₂ t
Full source 
@[to_additive]
protected theorem mul_apply [Mul X] [ContinuousMul X] {a₁ b₁ a₂ b₂ : X} (γ₁ : Path a₁ b₁)
    (γ₂ : Path a₂ b₂) (t : unitInterval) : (γ₁.mul γ₂) t = γ₁ t * γ₂ t :=
  rfl
Pointwise Product of Paths at Parameter $t$: $(\gamma_1 \cdot \gamma_2)(t) = \gamma_1(t) \cdot \gamma_2(t)$
Informal description
Let $X$ be a topological space equipped with a continuous multiplication operation. For any two paths $\gamma_1 \colon [0,1] \to X$ from $a_1$ to $b_1$ and $\gamma_2 \colon [0,1] \to X$ from $a_2$ to $b_2$, and for any $t \in [0,1]$, the pointwise product path $(\gamma_1 \cdot \gamma_2)(t)$ equals $\gamma_1(t) \cdot \gamma_2(t)$.
Path.truncate definition
{X : Type*} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ℝ) : Path (γ.extend <| min t₀ t₁) (γ.extend t₁)
Full source 
/-- `γ.truncate t₀ t₁` is the path which follows the path `γ` on the time interval `[t₀, t₁]`
and stays still otherwise. -/
def truncate {X : Type*} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ℝ) :
    Path (γ.extend <| min t₀ t₁) (γ.extend t₁) where
  toFun s := γ.extend (min (max s t₀) t₁)
  continuous_toFun :=
    γ.continuous_extend.comp ((continuous_subtype_val.max continuous_const).min continuous_const)
  source' := by
    simp only [min_def, max_def']
    split_ifs with h₁ h₂ h₃ h₄
    · simp [γ.extend_of_le_zero h₁]
    · congr
      linarith
    · have h₄ : t₁ ≤ 0 := le_of_lt (by simpa using h₂)
      simp [γ.extend_of_le_zero h₄, γ.extend_of_le_zero h₁]
    all_goals rfl
  target' := by
    simp only [min_def, max_def']
    split_ifs with h₁ h₂ h₃
    · simp [γ.extend_of_one_le h₂]
    · rfl
    · have h₄ : 1 ≤ t₀ := le_of_lt (by simpa using h₁)
      simp [γ.extend_of_one_le h₄, γ.extend_of_one_le (h₄.trans h₃)]
    · rfl
Truncated path
Informal description
Given a continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, and real numbers $t_0$ and $t_1$, the truncated path $\gamma.\text{truncate}(t_0, t_1)$ is the path that follows $\gamma$ on the interval $[\min(t_0, t_1), \max(t_0, t_1)]$ and remains constant outside this interval. Specifically, it is a path from $\gamma.\text{extend}(\min(t_0, t_1))$ to $\gamma.\text{extend}(t_1)$, where $\gamma.\text{extend}$ is the extension of $\gamma$ to the real line that is constant before $0$ and after $1$.
Path.truncateOfLE definition
{X : Type*} [TopologicalSpace X] {a b : X} (γ : Path a b) {t₀ t₁ : ℝ} (h : t₀ ≤ t₁) : Path (γ.extend t₀) (γ.extend t₁)
Full source 
/-- `γ.truncateOfLE t₀ t₁ h`, where `h : t₀ ≤ t₁` is `γ.truncate t₀ t₁`
casted as a path from `γ.extend t₀` to `γ.extend t₁`. -/
def truncateOfLE {X : Type*} [TopologicalSpace X] {a b : X} (γ : Path a b) {t₀ t₁ : ℝ}
    (h : t₀ ≤ t₁) : Path (γ.extend t₀) (γ.extend t₁) :=
  (γ.truncate t₀ t₁).cast (by rw [min_eq_left h]) rfl
Truncated path with ordered parameters
Informal description
Given a continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, and real numbers $t_0 \leq t_1$, the function returns the truncated path $\gamma.\text{truncate}(t_0, t_1)$ cast as a path from $\gamma.\text{extend}(t_0)$ to $\gamma.\text{extend}(t_1)$, where $\gamma.\text{extend}$ is the extension of $\gamma$ to the real line that is constant before $0$ and after $1$.
Path.truncate_range theorem
{a b : X} (γ : Path a b) {t₀ t₁ : ℝ} : range (γ.truncate t₀ t₁) ⊆ range γ
Full source 
theorem truncate_range {a b : X} (γ : Path a b) {t₀ t₁ : ℝ} :
    rangerange (γ.truncate t₀ t₁) ⊆ range γ := by
  rw [← γ.extend_range]
  simp only [range_subset_iff, SetCoe.exists, SetCoe.forall]
  intro x _hx
  simp only [DFunLike.coe, Path.truncate, mem_range_self]
Range Inclusion for Truncated Path
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, and for any real numbers $t_0, t_1$, the range of the truncated path $\gamma.\text{truncate}(t_0, t_1)$ is a subset of the range of $\gamma$. That is, \[ \text{range}(\gamma.\text{truncate}(t_0, t_1)) \subseteq \text{range}(\gamma). \]
Path.truncate_continuous_family theorem
{a b : X} (γ : Path a b) : Continuous (fun x => γ.truncate x.1 x.2.1 x.2.2 : ℝ × ℝ × I → X)
Full source 
/-- For a path `γ`, `γ.truncate` gives a "continuous family of paths", by which we mean
the uncurried function which maps `(t₀, t₁, s)` to `γ.truncate t₀ t₁ s` is continuous. -/
@[continuity]
theorem truncate_continuous_family {a b : X} (γ : Path a b) :
    Continuous (fun x => γ.truncate x.1 x.2.1 x.2.2 : ℝℝ × ℝ × I → X) :=
  γ.continuous_extend.comp
    (((continuous_subtype_val.comp (continuous_snd.comp continuous_snd)).max continuous_fst).min
      (continuous_fst.comp continuous_snd))
Continuity of the Truncated Path Family
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, the uncurried function $(t₀, t₁, s) \mapsto \gamma.\text{truncate}(t₀, t₁)(s)$ is continuous as a map from $\mathbb{R} \times \mathbb{R} \times [0,1]$ to $X$.
Path.truncate_const_continuous_family theorem
{a b : X} (γ : Path a b) (t : ℝ) : Continuous ↿(γ.truncate t)
Full source 
@[continuity]
theorem truncate_const_continuous_family {a b : X} (γ : Path a b)
    (t : ℝ) : Continuous ↿(γ.truncate t) := by
  have key : Continuous (fun x => (t, x) : ℝℝ × I → ℝℝ × ℝ × I) := by fun_prop
  exact γ.truncate_continuous_family.comp key
Continuity of the One-Parameter Truncated Path Family
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$ and any real number $t$, the uncurried function $(t', s) \mapsto \gamma.\text{truncate}(t, t')(s)$ is continuous as a map from $\mathbb{R} \times [0,1]$ to $X$.
Path.truncate_self theorem
{a b : X} (γ : Path a b) (t : ℝ) : γ.truncate t t = (Path.refl <| γ.extend t).cast (by rw [min_self]) rfl
Full source 
@[simp]
theorem truncate_self {a b : X} (γ : Path a b) (t : ℝ) :
    γ.truncate t t = (Path.refl <| γ.extend t).cast (by rw [min_self]) rfl := by
  ext x
  rw [cast_coe]
  simp only [truncate, DFunLike.coe, refl, min_def, max_def]
  split_ifs with h₁ h₂ <;> congr
Truncated Path at $(t,t)$ Equals Constant Path at $\gamma_{\text{ext}}(t)$
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$ and any real number $t$, the truncation of $\gamma$ at $(t, t)$ is equal to the constant path at $\gamma_{\text{ext}}(t)$, where $\gamma_{\text{ext}}$ is the extension of $\gamma$ to $\mathbb{R}$ that is constant before $0$ and after $1$.
Path.truncate_zero_zero theorem
{a b : X} (γ : Path a b) : γ.truncate 0 0 = (Path.refl a).cast (by rw [min_self, γ.extend_zero]) γ.extend_zero
Full source 
theorem truncate_zero_zero {a b : X} (γ : Path a b) :
    γ.truncate 0 0 = (Path.refl a).cast (by rw [min_self, γ.extend_zero]) γ.extend_zero := by
  convert γ.truncate_self 0
Truncated Path at $(0,0)$ Equals Constant Path at $a$
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, the truncation of $\gamma$ at the point $(0, 0)$ is equal to the constant path at $a$ (relabeled via `cast`), where the equality uses the fact that $\gamma_{\text{ext}}(0) = a$ and $\min(0, 0) = 0$.
Path.truncate_one_one theorem
{a b : X} (γ : Path a b) : γ.truncate 1 1 = (Path.refl b).cast (by rw [min_self, γ.extend_one]) γ.extend_one
Full source 
theorem truncate_one_one {a b : X} (γ : Path a b) :
    γ.truncate 1 1 = (Path.refl b).cast (by rw [min_self, γ.extend_one]) γ.extend_one := by
  convert γ.truncate_self 1
Truncated Path at $(1,1)$ Equals Constant Path at $b$
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, the truncation of $\gamma$ at the point $(1,1)$ is equal to the constant path at $b$ (with appropriate endpoint relabeling via `cast`), where $\gamma.\text{extend}(1) = b$ by definition.
Path.truncate_zero_one theorem
{a b : X} (γ : Path a b) : γ.truncate 0 1 = γ.cast (by simp [zero_le_one, extend_zero]) (by simp)
Full source 
@[simp]
theorem truncate_zero_one {a b : X} (γ : Path a b) :
    γ.truncate 0 1 = γ.cast (by simp [zero_le_one, extend_zero]) (by simp) := by
  ext x
  rw [cast_coe]
  have : ↑x ∈ (Icc 0 1 : Set ℝ) := x.2
  rw [truncate, coe_mk_mk, max_eq_left this.1, min_eq_left this.2, extend_extends']
Truncated Path at Endpoints Equals Original Path with Relabeling
Informal description
For any continuous path $\gamma$ from $a$ to $b$ in a topological space $X$, the truncation of $\gamma$ at the endpoints $0$ and $1$ is equal to $\gamma$ with its endpoints relabeled (via `cast`) using the properties that $\gamma.\text{extend}(0) = a$ and $\gamma.\text{extend}(1) = b$.
Path.reparam definition
(γ : Path x y) (f : I → I) (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Path x y
Full source 
/-- Given a path `γ` and a function `f : I → I` where `f 0 = 0` and `f 1 = 1`, `γ.reparam f` is the
path defined by `γ ∘ f`.
-/
def reparam (γ : Path x y) (f : I → I) (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
    Path x y where
  toFun := γ ∘ f
  continuous_toFun := by fun_prop
  source' := by simp [hf₀]
  target' := by simp [hf₁]
Reparametrization of a path
Informal description
Given a continuous path $\gamma$ from $x$ to $y$ in a topological space $X$ and a continuous function $f: [0,1] \to [0,1]$ with $f(0) = 0$ and $f(1) = 1$, the reparametrization $\gamma \circ f$ is a new path from $x$ to $y$ obtained by composing $\gamma$ with $f$.
Path.coe_reparam theorem
(γ : Path x y) {f : I → I} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : ⇑(γ.reparam f hfcont hf₀ hf₁) = γ ∘ f
Full source 
@[simp]
theorem coe_reparam (γ : Path x y) {f : I → I} (hfcont : Continuous f) (hf₀ : f 0 = 0)
    (hf₁ : f 1 = 1) : ⇑(γ.reparam f hfcont hf₀ hf₁) = γ ∘ f :=
  rfl
Function Representation of Reparametrized Path as Composition
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$ and any continuous function $f: [0,1] \to [0,1]$ satisfying $f(0) = 0$ and $f(1) = 1$, the underlying function of the reparametrized path $\gamma \circ f$ is equal to the composition of $\gamma$ with $f$.
Path.reparam_id theorem
(γ : Path x y) : γ.reparam id continuous_id rfl rfl = γ
Full source 
@[simp]
theorem reparam_id (γ : Path x y) : γ.reparam id continuous_id rfl rfl = γ := by
  ext
  rfl
Reparametrization by Identity Preserves Path
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$, the reparametrization of $\gamma$ by the identity function $\text{id} : [0,1] \to [0,1]$ is equal to $\gamma$ itself.
Path.range_reparam theorem
(γ : Path x y) {f : I → I} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : range (γ.reparam f hfcont hf₀ hf₁) = range γ
Full source 
theorem range_reparam (γ : Path x y) {f : I → I} (hfcont : Continuous f) (hf₀ : f 0 = 0)
    (hf₁ : f 1 = 1) : range (γ.reparam f hfcont hf₀ hf₁) = range γ := by
  change range (γ ∘ f) = range γ
  have : range f = univ := by
    rw [range_eq_univ]
    intro t
    have h₁ : Continuous (Set.IccExtend (zero_le_one' ℝ) f) := by continuity
    have := intermediate_value_Icc (zero_le_one' ℝ) h₁.continuousOn
    · rw [IccExtend_left, IccExtend_right, Icc.mk_zero, Icc.mk_one, hf₀, hf₁] at this
      rcases this t.2 with ⟨w, hw₁, hw₂⟩
      rw [IccExtend_of_mem _ _ hw₁] at hw₂
      exact ⟨_, hw₂⟩
  rw [range_comp, this, image_univ]
Range Preservation under Path Reparametrization
Informal description
For any continuous path $\gamma$ from $x$ to $y$ in a topological space $X$ and any continuous function $f: [0,1] \to [0,1]$ with $f(0) = 0$ and $f(1) = 1$, the range of the reparametrized path $\gamma \circ f$ is equal to the range of $\gamma$.
Path.refl_reparam theorem
{f : I → I} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : (refl x).reparam f hfcont hf₀ hf₁ = refl x
Full source 
theorem refl_reparam {f : I → I} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
    (refl x).reparam f hfcont hf₀ hf₁ = refl x := by
  ext
  simp
Reparametrization of Constant Path Yields Constant Path
Informal description
For any continuous function $f: [0,1] \to [0,1]$ such that $f(0) = 0$ and $f(1) = 1$, the reparametrization of the constant path at $x$ by $f$ is equal to the constant path at $x$. In other words, $(\text{refl } x) \circ f = \text{refl } x$.