Theorems · Theorem · algebraic topology
simply_connected_iff_paths_homotopic
∀ {Y : Type u_2} [inst : TopologicalSpace Y],
SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)A space is simply connected iff it is path connected, and there is at most one path up to homotopy between any two points.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 142 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.
Cites8
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
- Path.Homotopic.Quotientstatement and proof · cited by 55
- PathConnectedSpacestatement and proof · cited by 26
- SimplyConnectedSpacestatement and proof · cited by 19
- Path.Homotopic.setoidproof · cited by 14
- uniqueOfSubsingletonproof · cited by 9
- PathConnectedSpace.somePathproof · cited by 4
- simply_connected_iff_unique_homotopicproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- simply_connected_iff_paths_homotopic'proof · cited by 1