Theorems · Theorem · algebraic topology

Path.Homotopic.Quotient.trans_assoc

∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ x₂ x₃ : X} (γ₀ : Path.Homotopic.Quotient x₀ x₁)
  (γ₁ : Path.Homotopic.Quotient x₁ x₂) (γ₂ : Path.Homotopic.Quotient x₂ x₃),
  (γ₀.trans γ₁).trans γ₂ = γ₀.trans (γ₁.trans γ₂)

Defined in: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 135 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.

Cites6

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
Pathproof · cited by 318
Path.Homotopic.Quotientstatement and proof · cited by 55
Path.Homotopic.Quotient.transstatement · cited by 12
Path.Homotopic.Quotient.indproof · cited by 8
Path.Homotopic.trans_assocproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

simply_connected_iff_loops_nullhomotopicproof · cited by 1