Theorems · Theorem · general topology

Path.trans_apply

∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X} (γ : Path x y) (γ' : Path y z) (t : ↑unitInterval),
  (γ.trans γ') t = if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩

Defined in

Mathlib.Topology.Path

Cited by

9 results in Mathlib

Foundations

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

Assumes

TopologicalSpace