Properties along extended paths

Pointwise properties can be transferred between a path on unitInterval and its constant endpoint extension on all of ℝ. This lets statements about the extended curve use properties established on the original path. For the corresponding range equality, see Path.extend_range. Away from the joining parameter, a concatenation locally agrees with its rescaled component.

theorem Path.forall_extend_iff {E : Type u_1} [TopologicalSpace E] {p q : E} (γ : Path p q) {P : E → Prop} : (∀ (t : ℝ), P (γ.extend t)) ↔ ∀ (t : ↑unitInterval), P (γ t)

A property holds everywhere along an extended path exactly when it holds along the path.

theorem Path.eventuallyEq_extend_trans_of_lt_half {E : Type u_1} [TopologicalSpace E] {p q r : E} (γ : Path p q) (δ : Path q r) {t : ℝ} (ht : t < 1 / 2) : ⇑(γ.trans δ).extend =ᶠ[nhds t] fun (x : ℝ) => γ.extend (2 * x)

Below the joining parameter, an extended concatenation locally equals its first piece.

theorem Path.eventuallyEq_extend_trans_of_half_lt {E : Type u_1} [TopologicalSpace E] {p q r : E} (γ : Path p q) (δ : Path q r) {t : ℝ} (ht : 1 / 2 < t) : ⇑(γ.trans δ).extend =ᶠ[nhds t] fun (x : ℝ) => δ.extend (2 * x - 1)

Above the joining parameter, an extended concatenation locally equals its second piece.