Theorems · Theorem · algebraic topology

Path.Homotopy.hcomp_apply

∀ {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₁) (x : ↑unitInterval × ↑unitInterval),
  (F.hcomp G) x = if h : ↑x.2 ≤ 1 / 2 then (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩ else (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩

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