Theorems · Definition · algebraic topology
HomotopyGroup
Type u_3 → (X : Type u_4) → [TopologicalSpace X] → X → Type (max u_3 u_4)
The nth homotopy group at x defined as the quotient of Ω^n x by the
GenLoop.Homotopic relation.
- Defined in
- Mathlib.Topology.Homotopy.HomotopyGroup
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
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
Cited by13
Results whose statement or proof uses this declaration.
- HomotopyGroup.auxGroup_indepstatement and proof · cited by 2
- HomotopyGroup.auxGroupstatement · cited by 2
- HomotopyGroup.transAt_indepproof · cited by 1
- HomotopyGroup.isUnital_auxGroupstatement · cited by 1
- HomotopyGroup.symmAt_indepproof · cited by 1
- homotopyGroupEquivFundamentalGroupstatement · cited by 0
- homotopyGroupEquivFundamentalGroupOfUniquestatement · cited by 0
- homotopyGroupEquivZerothHomotopyOfIsEmptystatement · cited by 0
- HomotopyGroup.Piproof · cited by 0
- HomotopyGroup.homotopyGroupOfUniqueMulEquivFundamentalGroupstatement and proof · cited by 0
- HomotopyGroup.inv_specstatement · cited by 0
- HomotopyGroup.mul_specstatement and proof · cited by 0