Theorems · Definition · algebraic topology
unitInterval.uhpath01
FundamentalGroupoid.fromTop { down := 0 } ⟶ FundamentalGroupoid.fromTop { down := 1 }The homotopy path class of 0 → 1 in ULift I
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Quiver.Homstatement · cited by 32,603
- Realstatement · cited by 25,697
- CategoryTheory.Functor.objstatement · cited by 19,642
- Set.Elemstatement · cited by 7,166
- TopCatstatement · cited by 1,889
- CategoryTheory.Bundled.αstatement · cited by 736
- unitIntervalstatement · cited by 607
- CategoryTheory.Groupoidstatement · cited by 182
- FundamentalGroupoid.asproof · cited by 40
- CategoryTheory.Grpdstatement · cited by 30
- FundamentalGroupoid.fundamentalGroupoidFunctorstatement · cited by 21
Cited by3
Results whose statement or proof uses this declaration.
- ContinuousMap.Homotopy.evalAt_eqstatement · cited by 1
- ContinuousMap.Homotopy.eq_diag_pathproof · cited by 0
- ContinuousMap.Homotopy.diagonalPathproof · cited by 0