Theorems · Definition · general topology
Path.toContinuousMap
{X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → Path x y → C(↑unitInterval, X)- Defined in
- Mathlib.Topology.Path
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 114 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.
Cites7
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
- TopologicalSpacestatement and proof · cited by 24,529
- Set.Elemstatement · cited by 7,166
- ContinuousMapstatement · cited by 2,491
- unitIntervalstatement · cited by 607
- Pathstatement and proof · cited by 318
Cited by34
Results whose statement or proof uses this declaration.
- Path.Homotopyproof · cited by 21
- Path.prodproof · cited by 9
- Path.piproof · cited by 8
- GenLoop.fromLoopproof · cited by 8
- Path.continuousproof · cited by 3
- Path.Homotopy.eval_applystatement · cited by 2
- Path.Homotopy.reflproof · cited by 2
- TopCat.pathEquivproof · cited by 2
- IsCoveringMap.map_liftPathQuotientproof · cited by 2
- Path.toHomotopyConstproof · cited by 2
- IsLocalHomeomorph.existsUnique_continuousMap_liftsproof · cited by 2
- Path.target'statement · cited by 1