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 γ : C(ℝ, 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

structure Path {X : Type u_1} [TopologicalSpace X] (x y : X) extends C(↑unitInterval, X) : Type u_1

Continuous path connecting two points x and y in a topological space

• toFun : ↑unitInterval → X
• continuous_toFun : Continuous self.toFun
• source' : self.toFun 0 = x

  The start point of a Path.

• target' : self.toFun 1 = y

  The end point of a Path.

instance Path.instFunLike {X : Type u_1} [TopologicalSpace X] {x y : X} : FunLike (Path x y) (↑unitInterval) X

Equations

• Path.instFunLike = { coe := fun (γ : Path x y) => ⇑γ.toContinuousMap, coe_injective' := ⋯ }

instance Path.continuousMapClass {X : Type u_1} [TopologicalSpace X] {x y : X} : ContinuousMapClass (Path x y) (↑unitInterval) X

theorem Path.ext {X : Type u_1} [TopologicalSpace X] {x y : X} {γ₁ γ₂ : Path x y} : ⇑γ₁ = ⇑γ₂ → γ₁ = γ₂

theorem Path.ext_iff {X : Type u_1} [TopologicalSpace X] {x y : X} {γ₁ γ₂ : Path x y} : γ₁ = γ₂ ↔ ⇑γ₁ = ⇑γ₂

@[simp]

theorem Path.coe_mk' {X : Type u_1} [TopologicalSpace X] {x y : X} (f : C(↑unitInterval, X)) (h₁ : f.toFun 0 = x) (h₂ : f.toFun 1 = y) : ⇑{ toContinuousMap := f, source' := h₁, target' := h₂ } = ⇑f

A path constructed from a continuous map f has the same underlying function.

theorem Path.coe_mk_mk {X : Type u_1} [TopologicalSpace X] {x y : X} (f : ↑unitInterval → X) (h₁ : Continuous f) (h₂ : f 0 = x) (h₃ : f 1 = y) : ⇑{ toFun := f, continuous_toFun := h₁, source' := h₂, target' := h₃ } = f

theorem Path.continuous {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : Continuous ⇑γ

@[simp]

theorem Path.source {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : γ 0 = x

@[simp]

theorem Path.target {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : γ 1 = y

def Path.simps.apply {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : ↑unitInterval → X

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

• Path.simps.apply γ = ⇑γ

@[simp]

theorem Path.coe_toContinuousMap {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : ⇑γ.toContinuousMap = ⇑γ

@[deprecated ContinuousMap.coe_coe (since := "2025-05-02")]

theorem Path.coe_mk {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : ⇑↑γ = ⇑γ

A special version of ContinuousMap.coe_coe.

When you delete this deprecated lemma, please rename Path.coe_mk' to Path.coe_mk.

@[simp]

theorem Path.range_coe {X : Type u_1} [TopologicalSpace X] {x y : X} : Set.range _root_.toContinuousMap = {f : C(↑unitInterval, X) | f 0 = x ∧ f 1 = y}

instance Path.instHasUncurryPath {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {x y : α → X} : Function.HasUncurry ((a : α) → Path (x a) (y a)) (α × ↑unitInterval) X

Any function φ : Π (a : α), Path (x a) (y a) can be seen as a function α × I → X.

Equations

• Path.instHasUncurryPath = { uncurry := fun (φ : (a : α) → Path (x a) (y a)) (p : α × ↑unitInterval) => (φ p.1) p.2 }

@[simp]

theorem Path.source_mem_range {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : x ∈ Set.range ⇑γ

@[simp]

theorem Path.target_mem_range {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : y ∈ Set.range ⇑γ

def Path.refl {X : Type u_1} [TopologicalSpace X] (x : X) : Path x x

The constant path from a point to itself

Equations

• Path.refl x = { toContinuousMap := ContinuousMap.const (↑unitInterval) x, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.refl_apply {X : Type u_1} [TopologicalSpace X] (x : X) (x✝ : ↑unitInterval) : (refl x) x✝ = x

@[simp]

theorem Path.refl_range {X : Type u_1} [TopologicalSpace X] {a : X} : Set.range ⇑(refl a) = {a}

def Path.symm {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : Path y x

The reverse of a path from x to y, as a path from y to x

Equations

• γ.symm = { toFun := ⇑γ ∘ unitInterval.symm, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.symm_apply {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) (a✝ : ↑unitInterval) : γ.symm a✝ = (⇑γ ∘ unitInterval.symm) a✝

@[simp]

theorem Path.symm_symm {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : γ.symm.symm = γ

theorem Path.symm_bijective {X : Type u_1} [TopologicalSpace X] {x y : X} : Function.Bijective symm

@[simp]

theorem Path.refl_symm {X : Type u_1} [TopologicalSpace X] {a : X} : (refl a).symm = refl a

@[simp]

theorem Path.symm_range {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : Set.range ⇑γ.symm = Set.range ⇑γ

Space of paths

instance Path.instTopologicalSpace {X : Type u_1} [TopologicalSpace X] {x y : X} : TopologicalSpace (Path x y)

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.

Equations

• Path.instTopologicalSpace = TopologicalSpace.induced toContinuousMap ContinuousMap.compactOpen

instance Path.instContinuousEvalElemRealUnitInterval {X : Type u_1} [TopologicalSpace X] {x y : X} : ContinuousEval (Path x y) (↑unitInterval) X

theorem Path.continuous_uncurry_iff {X : Type u_1} [TopologicalSpace X] {x y : X} {Y : Type u_4} [TopologicalSpace Y] {g : Y → Path x y} : Continuous ↿g ↔ Continuous g

def Path.extend {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : C(ℝ, X)

A continuous map extending a path to ℝ, constant before 0 and after 1.

Equations

• γ.extend = { toFun := Set.IccExtend Path.extend._proof_1 ⇑γ, continuous_toFun := ⋯ }

theorem Continuous.pathExtend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} {γ : Y → Path x y} {f : Y → ℝ} (hγ : Continuous ↿γ) (hf : Continuous f) : Continuous fun (t : Y) => (γ t).extend (f t)

See Note [continuity lemma statement].

@[deprecated Continuous.pathExtend (since := "2025-05-02")]

theorem Continuous.path_extend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} {γ : Y → Path x y} {f : Y → ℝ} (hγ : Continuous ↿γ) (hf : Continuous f) : Continuous fun (t : Y) => (γ t).extend (f t)

Alias of Continuous.pathExtend.

---

See Note [continuity lemma statement].

theorem Path.continuous_extend {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : Continuous ⇑γ.extend

A useful special case of Continuous.path_extend.

theorem Filter.Tendsto.pathExtend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {l r : Y → X} {y : Y} {l₁ : Filter ℝ} {l₂ : Filter X} {γ : (y : Y) → Path (l y) (r y)} (hγ : Tendsto (↿γ) (nhds y ×ˢ map (Set.projIcc 0 1 ⋯) l₁) l₂) : Tendsto (↿fun (x : Y) => ⇑(γ x).extend) (nhds y ×ˢ l₁) l₂

@[deprecated Filter.Tendsto.pathExtend (since := "2025-05-02")]

theorem Filter.Tendsto.path_extend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {l r : Y → X} {y : Y} {l₁ : Filter ℝ} {l₂ : Filter X} {γ : (y : Y) → Path (l y) (r y)} (hγ : Tendsto (↿γ) (nhds y ×ˢ map (Set.projIcc 0 1 ⋯) l₁) l₂) : Tendsto (↿fun (x : Y) => ⇑(γ x).extend) (nhds y ×ˢ l₁) l₂

Alias of Filter.Tendsto.pathExtend.

theorem ContinuousAt.pathExtend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {g : Y → ℝ} {l r : Y → X} (γ : (y : Y) → Path (l y) (r y)) {y : Y} (hγ : ContinuousAt ↿γ (y, Set.projIcc 0 1 ⋯ (g y))) (hg : ContinuousAt g y) : ContinuousAt (fun (i : Y) => (γ i).extend (g i)) y

@[deprecated ContinuousAt.pathExtend (since := "2025-05-02")]

theorem ContinuousAt.path_extend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {g : Y → ℝ} {l r : Y → X} (γ : (y : Y) → Path (l y) (r y)) {y : Y} (hγ : ContinuousAt ↿γ (y, Set.projIcc 0 1 ⋯ (g y))) (hg : ContinuousAt g y) : ContinuousAt (fun (i : Y) => (γ i).extend (g i)) y

Alias of ContinuousAt.pathExtend.

@[simp]

theorem Path.extend_extends {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : γ.extend t = γ ⟨t, ht⟩

theorem Path.extend_zero {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : γ.extend 0 = x

theorem Path.extend_one {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : γ.extend 1 = y

theorem Path.extend_extends' {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t : ↑(Set.Icc 0 1)) : γ.extend ↑t = γ t

@[simp]

theorem Path.extend_range {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : Set.range ⇑γ.extend = Set.range ⇑γ

theorem Path.image_extend_of_subset {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) {s : Set ℝ} (h : unitInterval ⊆ s) : ⇑γ.extend '' s = Set.range ⇑γ

theorem Path.extend_of_le_zero {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) {t : ℝ} (ht : t ≤ 0) : γ.extend t = a

theorem Path.extend_of_one_le {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) {t : ℝ} (ht : 1 ≤ t) : γ.extend t = b

@[simp]

theorem Path.refl_extend {X : Type u_1} [TopologicalSpace X] {a : X} : (refl a).extend = ContinuousMap.const ℝ a

theorem Path.extend_symm_apply {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) (t : ℝ) : γ.symm.extend t = γ.extend (1 - t)

@[simp]

theorem Path.extend_symm {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : ⇑γ.symm.extend = fun (x_1 : ℝ) => γ.extend (1 - x_1)

def Path.ofLine {X : Type u_1} [TopologicalSpace X] {x y : X} {f : ℝ → X} (hf : ContinuousOn f unitInterval) (h₀ : f 0 = x) (h₁ : f 1 = y) : Path x y

The path obtained from a map defined on ℝ by restriction to the unit interval.

Equations

• Path.ofLine hf h₀ h₁ = { toFun := f ∘ Subtype.val, continuous_toFun := ⋯, source' := h₀, target' := h₁ }

theorem Path.ofLine_mem {X : Type u_1} [TopologicalSpace X] {x y : X} {f : ℝ → X} (hf : ContinuousOn f unitInterval) (h₀ : f 0 = x) (h₁ : f 1 = y) (t : ↑unitInterval) : (ofLine hf h₀ h₁) t ∈ f '' unitInterval

@[simp]

theorem Path.ofLine_extend {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : ofLine ⋯ ⋯ ⋯ = γ

def Path.trans {X : Type u_1} [TopologicalSpace X] {x y z : X} (γ : Path x y) (γ' : Path y z) : Path x z

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

Equations

• γ.trans γ' = { toFun := (fun (t : ℝ) => if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ Subtype.val, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

theorem Path.trans_apply {X : Type u_1} [TopologicalSpace X] {x y z : X} (γ : Path x y) (γ' : Path y z) (t : ↑unitInterval) : (γ.trans γ') t = if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩

@[simp]

theorem Path.trans_symm {X : Type u_1} [TopologicalSpace X] {x y z : X} (γ : Path x y) (γ' : Path y z) : (γ.trans γ').symm = γ'.symm.trans γ.symm

theorem Path.extend_trans_of_le_half {X : Type u_1} [TopologicalSpace X] {x y z : X} (γ₁ : Path x y) (γ₂ : Path y z) {t : ℝ} (ht : t ≤ 1 / 2) : (γ₁.trans γ₂).extend t = γ₁.extend (2 * t)

theorem Path.extend_trans_of_half_le {X : Type u_1} [TopologicalSpace X] {x y z : X} (γ₁ : Path x y) (γ₂ : Path y z) {t : ℝ} (ht : 1 / 2 ≤ t) : (γ₁.trans γ₂).extend t = γ₂.extend (2 * t - 1)

@[simp]

theorem Path.refl_trans_refl {X : Type u_1} [TopologicalSpace X] {a : X} : (refl a).trans (refl a) = refl a

theorem Path.trans_range {X : Type u_1} [TopologicalSpace X] {a b c : X} (γ₁ : Path a b) (γ₂ : Path b c) : Set.range ⇑(γ₁.trans γ₂) = Set.range ⇑γ₁ ∪ Set.range ⇑γ₂

def Path.map' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} (γ : Path x y) {f : X → Y} (h : ContinuousOn f (Set.range ⇑γ)) : Path (f x) (f y)

Image of a path from x to y by a map which is continuous on the path.

Equations

• γ.map' h = { toFun := f ∘ ⇑γ, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

def Path.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} (γ : Path x y) {f : X → Y} (h : Continuous f) : Path (f x) (f y)

Image of a path from x to y by a continuous map

Equations

• γ.map h = γ.map' ⋯

@[simp]

theorem Path.map_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} (γ : Path x y) {f : X → Y} (h : Continuous f) : ⇑(γ.map h) = f ∘ ⇑γ

@[simp]

theorem Path.map_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} (γ : Path x y) {f : X → Y} (h : Continuous f) : (γ.map h).symm = γ.symm.map h

@[simp]

theorem Path.map_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y z : X} (γ : Path x y) (γ' : Path y z) {f : X → Y} (h : Continuous f) : (γ.trans γ').map h = (γ.map h).trans (γ'.map h)

@[simp]

theorem Path.map_id {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : γ.map ⋯ = γ

@[simp]

theorem Path.map_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} (γ : Path x y) {Z : Type u_4} [TopologicalSpace Z] {f : X → Y} (hf : Continuous f) {g : Y → Z} (hg : Continuous g) : (γ.map hf).map hg = γ.map ⋯

def Path.cast {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) {x' y' : X} (hx : x' = x) (hy : y' = y) : Path x' y'

Casting a path from x to y to a path from x' to y' when x' = x and y' = y

Equations

• γ.cast hx hy = { toFun := ⇑γ, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.cast_rfl_rfl {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : γ.cast ⋯ ⋯ = γ

@[simp]

theorem Path.symm_cast {X : Type u_1} [TopologicalSpace X] {a₁ a₂ b₁ b₂ : X} (γ : Path a₂ b₂) (ha : a₁ = a₂) (hb : b₁ = b₂) : (γ.cast ha hb).symm = γ.symm.cast hb ha

@[simp]

theorem Path.trans_cast {X : Type u_1} [TopologicalSpace X] {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

@[simp]

theorem Path.extend_cast {X : Type u_1} [TopologicalSpace X] {x y x' y' : X} (γ : Path x y) (hx : x' = x) (hy : y' = y) : (γ.cast hx hy).extend = γ.extend

@[simp]

theorem Path.cast_coe {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) {x' y' : X} (hx : x' = x) (hy : y' = y) : ⇑(γ.cast hx hy) = ⇑γ

theorem Path.bijective_cast {X : Type u_1} [TopologicalSpace X] {x y x' y' : X} (hx : x' = x) (hy : y' = y) : Function.Bijective fun (x_1 : Path x y) => x_1.cast hx hy

theorem Path.exists_congr {X : Type u_1} [TopologicalSpace X] {x₁ x₂ y₁ y₂ : X} {p : Path x₁ y₁ → Prop} (hx : x₁ = x₂) (hy : y₁ = y₂) : (∃ (γ : Path x₁ y₁), p γ) ↔ ∃ (γ : Path x₂ y₂), p (γ.cast hx hy)

theorem Path.symm_continuous_family {X : Type u_1} [TopologicalSpace X] {ι : Type u_4} [TopologicalSpace ι] {a b : ι → X} (γ : (t : ι) → Path (a t) (b t)) (h : Continuous ↿γ) : Continuous ↿fun (t : ι) => (γ t).symm

theorem Path.continuous_symm {X : Type u_1} [TopologicalSpace X] {x y : X} : Continuous symm

theorem Path.continuous_uncurry_extend_of_continuous_family {X : Type u_1} [TopologicalSpace X] {ι : Type u_4} [TopologicalSpace ι] {a b : ι → X} (γ : (t : ι) → Path (a t) (b t)) (h : Continuous ↿γ) : Continuous ↿fun (t : ι) => ⇑(γ t).extend

theorem Path.trans_continuous_family {X : Type u_1} [TopologicalSpace X] {ι : Type u_4} [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)

theorem Continuous.path_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y z : X} {f : Y → Path x y} {g : Y → Path y z} : Continuous f → Continuous g → Continuous fun (t : Y) => (f t).trans (g t)

theorem Path.continuous_trans {X : Type u_1} [TopologicalSpace X] {x y z : X} : Continuous fun (ρ : Path x y × Path y z) => ρ.1.trans ρ.2

Product of paths

def Path.prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a₁ a₂ : X} {b₁ b₂ : Y} (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : Path (a₁, b₁) (a₂, b₂)

Given a path in X and a path in Y, we can take their pointwise product to get a path in X × Y.

Equations

• γ₁.prod γ₂ = { toContinuousMap := γ₁.prodMk γ₂.toContinuousMap, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.prod_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a₁ a₂ : X} {b₁ b₂ : Y} (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : ⇑(γ₁.prod γ₂) = fun (t : ↑unitInterval) => (γ₁ t, γ₂ t)

theorem Path.trans_prod_eq_prod_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a₁ a₂ a₃ : X} {b₁ b₂ b₃ : Y} (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂) (δ₂ : Path b₂ b₃) : (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)

Path composition commutes with products

def Path.pi {ι : Type u_3} {χ : ι → Type u_4} [(i : ι) → TopologicalSpace (χ i)] {as bs : (i : ι) → χ i} (γ : (i : ι) → Path (as i) (bs i)) : Path as bs

Given a family of paths, one in each Xᵢ, we take their pointwise product to get a path in Π i, Xᵢ.

Equations

• Path.pi γ = { toContinuousMap := ContinuousMap.pi fun (i : ι) => (γ i).toContinuousMap, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.pi_coe {ι : Type u_3} {χ : ι → Type u_4} [(i : ι) → TopologicalSpace (χ i)] {as bs : (i : ι) → χ i} (γ : (i : ι) → Path (as i) (bs i)) : ⇑(Path.pi γ) = fun (t : ↑unitInterval) (i : ι) => (γ i) t

theorem Path.trans_pi_eq_pi_trans {ι : Type u_3} {χ : ι → Type u_4} [(i : ι) → TopologicalSpace (χ i)] {as bs cs : (i : ι) → χ i} (γ₀ : (i : ι) → Path (as i) (bs i)) (γ₁ : (i : ι) → Path (bs i) (cs i)) : (Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun (i : ι) => (γ₀ i).trans (γ₁ i)

Path composition commutes with products

Pointwise operations on paths in a topological (additive) group

def Path.mul {X : Type u_1} [TopologicalSpace X] [Mul X] [ContinuousMul X] {a₁ b₁ a₂ b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) : Path (a₁ * a₂) (b₁ * b₂)

Pointwise multiplication of paths in a topological group.

Equations

• γ₁.mul γ₂ = (γ₁.prod γ₂).map ⋯

def Path.add {X : Type u_1} [TopologicalSpace X] [Add X] [ContinuousAdd X] {a₁ b₁ a₂ b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) : Path (a₁ + a₂) (b₁ + b₂)

Pointwise addition of paths in a topological additive group.

Equations

• γ₁.add γ₂ = (γ₁.prod γ₂).map ⋯

@[simp]

theorem Path.add_apply {X : Type u_1} [TopologicalSpace X] [Add X] [ContinuousAdd X] {a₁ b₁ a₂ b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) (a✝ : ↑unitInterval) : (γ₁.add γ₂) a✝ = γ₁ a✝ + γ₂ a✝

@[simp]

theorem Path.mul_apply {X : Type u_1} [TopologicalSpace X] [Mul X] [ContinuousMul X] {a₁ b₁ a₂ b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) (a✝ : ↑unitInterval) : (γ₁.mul γ₂) a✝ = γ₁ a✝ * γ₂ a✝

def Path.inv {X : Type u_1} [TopologicalSpace X] {a b : X} [Inv X] [ContinuousInv X] (γ : Path a b) : Path a⁻¹ b⁻¹

Pointwise inversion of paths in a topological group.

Equations

• γ.inv = γ.map ⋯

def Path.neg {X : Type u_1} [TopologicalSpace X] {a b : X} [Neg X] [ContinuousNeg X] (γ : Path a b) : Path (-a) (-b)

Pointwise negation of paths in a topological group.

Equations

• γ.neg = γ.map ⋯

@[simp]

theorem Path.neg_apply {X : Type u_1} [TopologicalSpace X] {a b : X} [Neg X] [ContinuousNeg X] (γ : Path a b) (a✝ : ↑unitInterval) : γ.neg a✝ = -γ a✝

@[simp]

theorem Path.inv_apply {X : Type u_1} [TopologicalSpace X] {a b : X} [Inv X] [ContinuousInv X] (γ : Path a b) (a✝ : ↑unitInterval) : γ.inv a✝ = (γ a✝)⁻¹

Truncating a path

def Path.truncate {X : Type u_4} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ℝ) : Path (γ.extend (min t₀ t₁)) (γ.extend t₁)

γ.truncate t₀ t₁ is the path which follows the path γ on the time interval [t₀, t₁] and stays still otherwise.

Equations

• γ.truncate t₀ t₁ = { toFun := fun (s : ↑unitInterval) => γ.extend (min (max (↑s) t₀) t₁), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

def Path.truncateOfLE {X : Type u_4} [TopologicalSpace X] {a b : X} (γ : Path a b) {t₀ t₁ : ℝ} (h : t₀ ≤ t₁) : Path (γ.extend t₀) (γ.extend t₁)

γ.truncateOfLE t₀ t₁ h, where h : t₀ ≤ t₁ is γ.truncate t₀ t₁ casted as a path from γ.extend t₀ to γ.extend t₁.

Equations

• γ.truncateOfLE h = (γ.truncate t₀ t₁).cast ⋯ ⋯

theorem Path.truncate_range {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) {t₀ t₁ : ℝ} : Set.range ⇑(γ.truncate t₀ t₁) ⊆ Set.range ⇑γ

theorem Path.truncate_continuous_family {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : Continuous fun (x : ℝ × ℝ × ↑unitInterval) => (γ.truncate x.1 x.2.1) x.2.2

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.

theorem Path.truncate_const_continuous_family {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t : ℝ) : Continuous ↿(γ.truncate t)

@[simp]

theorem Path.truncate_self {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t : ℝ) : γ.truncate t t = (refl (γ.extend t)).cast ⋯ ⋯

theorem Path.truncate_zero_zero {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : γ.truncate 0 0 = (refl a).cast ⋯ ⋯

theorem Path.truncate_one_one {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : γ.truncate 1 1 = (refl b).cast ⋯ ⋯

@[simp]

theorem Path.truncate_zero_one {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : γ.truncate 0 1 = γ.cast ⋯ ⋯

Reparametrising a path

def Path.reparam {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) (f : ↑unitInterval → ↑unitInterval) (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Path x y

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.

Equations

• γ.reparam f hfcont hf₀ hf₁ = { toFun := ⇑γ ∘ f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.coe_reparam {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) {f : ↑unitInterval → ↑unitInterval} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : ⇑(γ.reparam f hfcont hf₀ hf₁) = ⇑γ ∘ f

@[simp]

theorem Path.reparam_id {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) : γ.reparam id ⋯ ⋯ ⋯ = γ

theorem Path.range_reparam {X : Type u_1} [TopologicalSpace X] {x y : X} (γ : Path x y) {f : ↑unitInterval → ↑unitInterval} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Set.range ⇑(γ.reparam f hfcont hf₀ hf₁) = Set.range ⇑γ

theorem Path.refl_reparam {X : Type u_1} [TopologicalSpace X] {x : X} {f : ↑unitInterval → ↑unitInterval} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : (refl x).reparam f hfcont hf₀ hf₁ = refl x