@[simp]

theorem Path.extend_div_self {X : Type u_1} [TopologicalSpace X] {x : X} (γ : Path x x) (t : ℝ) : γ.extend (t / t) = x

A loop evaluated at t / t is equal to its endpoint. Note that t / t = 0 for t = 0.

def Path.strans {X : Type u_1} [TopologicalSpace X] {x : X} (γ γ' : Path x x) (t₀ : ↑unitInterval) : Path x x

Concatenation of two loops which moves through the first loop on [0, t₀] and through the second one on [t₀, 1]. All endpoints are assumed to be the same so that this function is also well-defined for t₀ ∈ {0, 1}. strans stands either for a skewed transitivity, or a transitivity with different speeds.

Equations

• γ.strans γ' t₀ = { toFun := fun (t : ↑unitInterval) => if t ≤ t₀ then γ.extend (↑t / ↑t₀) else γ'.extend ((↑t - ↑t₀) / (1 - ↑t₀)), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

theorem Path.strans_def {X : Type u_1} [TopologicalSpace X] {x : X} {t₀ t : ↑unitInterval} (γ γ' : Path x x) : (γ.strans γ' t₀) t = if h : t ≤ t₀ then γ ⟨↑t / ↑t₀, ⋯⟩ else γ' ⟨(↑t - ↑t₀) / (1 - ↑t₀), ⋯⟩

Reformulate strans without using extend. This is useful to not have to prove that the arguments to γ lie in I after this.

@[simp]

theorem Path.strans_of_ge {X : Type u_1} [TopologicalSpace X] {x : X} {γ γ' : Path x x} {t t₀ : ↑unitInterval} (h : t₀ ≤ t) : (γ.strans γ' t₀) t = γ'.extend ((↑t - ↑t₀) / (1 - ↑t₀))

theorem Path.unitInterval.zero_le (x : ↑unitInterval) : 0 ≤ x

@[simp]

theorem Path.strans_zero {X : Type u_1} [TopologicalSpace X] {x : X} (γ γ' : Path x x) : γ.strans γ' 0 = γ'

@[simp]

theorem Path.strans_one {X : Type u_1} [TopologicalSpace X] {x : X} (γ γ' : Path x x) : γ.strans γ' 1 = γ

theorem Path.strans_self {X : Type u_1} [TopologicalSpace X] {x : X} (γ γ' : Path x x) (t₀ : ↑unitInterval) : (γ.strans γ' t₀) t₀ = x

@[simp]

theorem Path.refl_strans_refl {X : Type u_1} [TopologicalSpace X] {x : X} {t₀ : ↑unitInterval} : (refl x).strans (refl x) t₀ = refl x

theorem Path.subset_range_strans_left {X : Type u_1} [TopologicalSpace X] {x : X} {γ γ' : Path x x} {t₀ : ↑unitInterval} (h : t₀ ≠ 0) : Set.range ⇑γ ⊆ Set.range ⇑(γ.strans γ' t₀)

theorem Path.subset_range_strans_right {X : Type u_1} [TopologicalSpace X] {x : X} {γ γ' : Path x x} {t₀ : ↑unitInterval} (h : t₀ ≠ 1) : Set.range ⇑γ' ⊆ Set.range ⇑(γ.strans γ' t₀)

theorem Path.range_strans_subset {X : Type u_1} [TopologicalSpace X] {x : X} {γ γ' : Path x x} {t₀ : ↑unitInterval} : Set.range ⇑(γ.strans γ' t₀) ⊆ Set.range ⇑γ ∪ Set.range ⇑γ'

theorem Path.Continuous.path_strans {X : Type u_5} {Y : Type u_6} [UniformSpace X] [LocallyCompactSpace X] [UniformSpace Y] {f : X → Y} {t s : X → ↑unitInterval} {γ γ' : (x : X) → Path (f x) (f x)} (hγ : Continuous ↿γ) (hγ' : Continuous ↿γ') (hγ0 : ∀ ⦃x : X⦄ ⦃s : ↑unitInterval⦄, t x = 0 → (γ x) s = f x) (hγ'1 : ∀ ⦃x : X⦄ ⦃s : ↑unitInterval⦄, t x = 1 → (γ' x) s = f x) (ht : Continuous t) (hs : Continuous s) : Continuous fun (x : X) => ((γ x).strans (γ' x) (t x)) (s x)