LeanPool.DirectedTopologyLean4.SplitPath.SplitDipath #

source

theorem SplitDipath.first_part_is_dipath {X : Type u} [DirectedSpace X] {x₀ x₁ : X} {γ : Path x₀ x₁} (γ_dipath : IsDipath γ) (T : ↑unitInterval) :

IsDipath (SplitPath.FirstPart γ T)

source

theorem SplitDipath.second_part_is_dipath {X : Type u} [DirectedSpace X] {x₀ x₁ : X} {γ : Path x₀ x₁} (γ_dipath : IsDipath γ) (T : ↑unitInterval) :

IsDipath (SplitPath.SecondPart γ T)

source

def SplitDipath.FirstPart {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) (T : ↑unitInterval) :

Dipath x₀ (γ T)

The first half of a dipath split at parameter T, viewed as a dipath from γ 0 to γ T.

Equations

SplitDipath.FirstPart γ T = { toPath := SplitPath.FirstPart γ.toPath T, dipath_toPath := ⋯ }

Instances For

source

def SplitDipath.SecondPart {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) (T : ↑unitInterval) :

Dipath (γ T) x₁

The second half of a dipath split at parameter T, viewed as a dipath from γ T to γ 1.

Equations

SplitDipath.SecondPart γ T = { toPath := SplitPath.SecondPart γ.toPath T, dipath_toPath := ⋯ }

Instances For

source

@[simp]

theorem SplitDipath.first_part_apply {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) (T t : ↑unitInterval) :

(FirstPart γ T) t = γ ⟨↑T * ↑t, ⋯⟩

source

@[simp]

theorem SplitDipath.second_part_apply {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) (T t : ↑unitInterval) :

(SecondPart γ T) t = γ ⟨↑(unitInterval.symm T) * ↑t + ↑T, ⋯⟩

source

noncomputable def SplitDipath.transReparamMap {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) :

D(↑unitInterval,↑unitInterval)

The reparametrization of I used to glue the first and second part of a dipath split at T back into the original dipath, packaged as a directed self-map of I.

Equations

SplitDipath.transReparamMap hT₀ hT₁ = { toFun := fun (t : ↑unitInterval) => ⟨SplitPath.transReparam T t, ⋯⟩, continuous_toFun := ⋯, directed_toFun := ⋯ }

Instances For

source

theorem SplitDipath.trans_reparam_map_zero {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) :

(transReparamMap hT₀ hT₁) 0 = 0

source

theorem SplitDipath.trans_reparam_map_one {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) :

(transReparamMap hT₀ hT₁) 1 = 1

source

theorem SplitDipath.first_trans_second_reparam_eq_self {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (γ : Dipath x₀ x₁) {T : ↑unitInterval} (hT₀ : 0 < T) (hT₁ : T < 1) :

γ = ((FirstPart γ T).trans (SecondPart γ T)).reparam (transReparamMap hT₀ hT₁) ⋯ ⋯