Theorems · Theorem · algebraic topology

Path.Homotopic.prod_lift

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {a₁ a₂ : α} {b₁ b₂ : β}
  (p₁ : Path a₁ a₂) (p₂ : Path b₁ b₂),
  Path.Homotopic.prod (Path.Homotopic.Quotient.mk p₁) (Path.Homotopic.Quotient.mk p₂) =
    Path.Homotopic.Quotient.mk (p₁.prod p₂)

Defined in

Mathlib.Topology.Homotopy.Product

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace