LeanPool.DirectedTopologyLean4.StretchPath

theorem Dipath.double_mem_I_of_bounded {t₀ t₁ : ↑unitInterval} (t : ↑unitInterval) (γ : Dipath t₀ t₁) (ht₁ : ↑t₁ ≤ 2⁻¹) : 2 * ↑(γ t) ∈ unitInterval

def Dipath.stretchUpPath {t₀ t₁ : ↑unitInterval} (γ : Dipath t₀ t₁) (ht₁ : ↑t₁ ≤ 2⁻¹) : Path ⟨2 * ↑t₀, ⋯⟩ ⟨2 * ↑t₁, ⋯⟩

Stretch a path whose image lies in [0, 1/2] to a path on the full unit interval by doubling all parameter values.

Equations

• γ.stretchUpPath ht₁ = { toFun := fun (t : ↑unitInterval) => ⟨2 * ↑(γ t), ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

theorem Dipath.isDipath_stretch_up {t₀ t₁ : ↑unitInterval} (γ : Dipath t₀ t₁) (ht₁ : ↑t₁ ≤ 2⁻¹) : IsDipath (γ.stretchUpPath ht₁)

def Dipath.stretchUp {t₀ t₁ : ↑unitInterval} (γ : Dipath t₀ t₁) (ht₁ : ↑t₁ ≤ 2⁻¹) : Dipath ⟨2 * ↑t₀, ⋯⟩ ⟨2 * ↑t₁, ⋯⟩

The dipath obtained by stretching a dipath whose image lies in [0, 1/2] to the full unit interval.

Equations

• γ.stretchUp ht₁ = { toPath := γ.stretchUpPath ht₁, dipath_toPath := ⋯ }

theorem Dipath.double_sub_one_mem_I_of_bounded {t₀ t₁ : ↑unitInterval} (t : ↑unitInterval) (γ : Dipath t₀ t₁) (ht₀ : 2⁻¹ ≤ ↑t₀) : 2 * ↑(γ t) - 1 ∈ unitInterval

def Dipath.stretchDownPath {t₀ t₁ : ↑unitInterval} (γ : Dipath t₀ t₁) (ht₀ : 2⁻¹ ≤ ↑t₀) : Path ⟨2 * ↑t₀ - 1, ⋯⟩ ⟨2 * ↑t₁ - 1, ⋯⟩

Stretch a path whose image lies in [1/2, 1] to a path on the full unit interval by mapping each parameter s to 2s - 1.

Equations

• γ.stretchDownPath ht₀ = { toFun := fun (t : ↑unitInterval) => ⟨2 * ↑(γ t) - 1, ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

theorem Dipath.isDipath_stretch_down {t₀ t₁ : ↑unitInterval} (γ : Dipath t₀ t₁) (ht₀ : 2⁻¹ ≤ ↑t₀) : IsDipath (γ.stretchDownPath ht₀)

def Dipath.stretchDown {t₀ t₁ : ↑unitInterval} (γ : Dipath t₀ t₁) (ht₀ : 2⁻¹ ≤ ↑t₀) : Dipath ⟨2 * ↑t₀ - 1, ⋯⟩ ⟨2 * ↑t₁ - 1, ⋯⟩

The dipath obtained by stretching a dipath whose image lies in [1/2, 1] to the full unit interval.

Equations

• γ.stretchDown ht₀ = { toPath := γ.stretchDownPath ht₀, dipath_toPath := ⋯ }