LeanPool.DirectedTopologyLean4.TransRefl

theorem Dipath.Dihomotopy.directed_transReflReparamAux : DirectedMap.Directed { toFun := fun (t : ↑unitInterval) => ⟨Path.Homotopy.transReflReparamAux t, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def Dipath.Dihomotopy.TransReflReparamAuxMap : D(↑unitInterval,↑unitInterval)

The auxiliary reparametrization map I → I used to show that p.trans (refl _) is dihomotopic to p, packaged as a directed map.

Equations

• One or more equations did not get rendered due to their size.

theorem Dipath.Dihomotopy.trans_refl_reparam_dipath {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (p : Dipath x₀ x₁) : p.trans (refl x₁) = p.reparam TransReflReparamAuxMap ⋯ ⋯

noncomputable def Dipath.Dihomotopy.ReflTransReparamAux (t : ↑unitInterval) : ℝ

Auxilliary function for ReflTransReparam

Equations

• Dipath.Dihomotopy.ReflTransReparamAux t = if ↑t ≤ 1 / 2 then 0 else 2 * ↑t - 1

theorem Dipath.Dihomotopy.continuous_ReflTransReparamAux : Continuous ReflTransReparamAux

theorem Dipath.Dihomotopy.reflTransReparamAux_mem_I (t : ↑unitInterval) : ReflTransReparamAux t ∈ unitInterval

theorem Dipath.Dihomotopy.reflTransReparamAux_zero : ReflTransReparamAux 0 = 0

theorem Dipath.Dihomotopy.reflTransReparamAux_one : ReflTransReparamAux 1 = 1

theorem Dipath.Dihomotopy.directed_ReflTransReparamAux : DirectedMap.Directed { toFun := fun (t : ↑unitInterval) => ⟨ReflTransReparamAux t, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def Dipath.Dihomotopy.ReflTransReparamAuxMap : D(↑unitInterval,↑unitInterval)

The auxiliary reparametrization map I → I used to show that (refl _).trans p is dihomotopic to p, packaged as a directed map.

Equations

• One or more equations did not get rendered due to their size.

theorem Dipath.Dihomotopy.refl_trans_reparam {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : (Path.refl x₀).trans p = p.reparam (fun (t : ↑unitInterval) => ⟨ReflTransReparamAux t, ⋯⟩) ⋯ ⋯ ⋯

theorem Dipath.Dihomotopy.refl_trans_reparam_dipath {X : Type u} [DirectedSpace X] {x₀ x₁ : X} (p : Dipath x₀ x₁) : (refl x₀).trans p = p.reparam ReflTransReparamAuxMap ⋯ ⋯