Theorems · Definition · general topology

Path.truncate

{X : Type u_4} →
  [inst : TopologicalSpace X] → {a b : X} → (γ : Path a b) → (t₀ t₁ : ℝ) → Path (γ.extend (min t₀ t₁)) (γ.extend t₁)

γ.truncate t₀ t₁ is the path which follows the path γ on the time interval [t₀, t₁] and stays still otherwise.

Defined in

Mathlib.Topology.Path

Cited by

7 results in Mathlib

Foundations

Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace