Theorems · Theorem · algebraic topology

Path.Homotopy.hcomp_half

∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ x₂ : X} {p₀ q₀ : Path x₀ x₁} {p₁ q₁ : Path x₁ x₂} (F : p₀.Homotopy q₀)
  (G : p₁.Homotopy q₁) (t : ↑unitInterval), (F.hcomp G) (t, ⟨1 / 2, ⋯⟩) = x₁

Defined in

Mathlib.Topology.Homotopy.Path

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace