Theorems · Definition · algebraic topology

Path.Homotopic.pi

{ι : Type u_1} →
  {X : ι → Type u_2} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {as bs : (i : ι) → X i} → ((i : ι) → Path.Homotopic.Quotient (as i) (bs i)) → Path.Homotopic.Quotient as bs

The product of a family of path homotopy classes.

Defined in: Mathlib.Topology.Homotopy.Product
Cited by: 5 results in Mathlib
Foundations: Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
Path.Homotopic.Quotientstatement and proof · cited by 55
Path.piproof · cited by 8
Quotient.mapproof · cited by 7
Quotient.choiceproof · cited by 2

Cited by6

Results whose statement or proof uses this declaration.

Path.Homotopic.pi_liftstatement · cited by 3
FundamentalGroupoidFunctor.piToPiTopproof · cited by 3
Path.Homotopic.comp_pi_eq_pi_compstatement and proof · cited by 0
Path.Homotopic.pi_projstatement · cited by 0
FundamentalGroupoidFunctor.piToPiTop_mapstatement · cited by 0
Path.Homotopic.proj_pistatement and proof · cited by 0