Mathlib Map

Theorems · Definition · algebraic topology

unitInterval.upath01

Path { down := 0 } { down := 1 }

The path 0 ⟶ 1 in ULift I

Defined in
Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
Cited by
1 results in Mathlib
Foundations
Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

unitInterval.uhpath01 · cited by 2unitInterval.uhpath01ContinuousMap.Homotopy.evalAt_eq · cited by 1Homotopy.evalAt_eqSet · cited by 53352SetReal · cited by 25697RealSet.Elem · cited by 7166Set.ElemunitInterval · cited by 607unitIntervalPath · cited by 318PathunitInterval.upath01CITED BYCITES

Cites5

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

  • Setstatement · cited by 53,352
  • Realstatement · cited by 25,697
  • Set.Elemstatement · cited by 7,166
  • unitIntervalstatement · cited by 607
  • Pathstatement · cited by 318

Cited by2

Results whose statement or proof uses this declaration.