Theorems · Definition · general topology
Path.refl
{X : Type u_1} → [inst : TopologicalSpace X] → (x : X) → Path x xThe constant path from a point to itself
- Defined in
- Mathlib.Topology.Path
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 115 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.
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
- Set.Elemproof · cited by 7,166
- ContinuousMapproof · cited by 2,491
- unitIntervalproof · cited by 607
- Pathstatement · cited by 318
- ContinuousMap.constproof · cited by 45
Cited by45
Results whose statement or proof uses this declaration.
- Path.refl_applystatement and proof · cited by 11
- Path.Homotopic.Quotient.reflproof · cited by 9
- Path.concatproof · cited by 7
- Path.Homotopy.reflTransstatement · cited by 4
- Path.concat_zerostatement and proof · cited by 3
- Path.concat_succproof · cited by 3
- Joined.reflproof · cited by 3
- Path.refl_rangestatement · cited by 3
- JoinedIn.reflproof · cited by 3
- curveIntegral_reflstatement and proof · cited by 2
- IsPathConnected.exists_path_through_familyproof · cited by 2
- Path.truncate_selfstatement · cited by 2