Theorems · Theorem · algebraic topology
simply_connected_iff_loops_nullhomotopic
∀ {Y : Type u_2} [inst : TopologicalSpace Y],
SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x : Y) (γ : Path x x), γ.Homotopic (Path.refl x)A space is simply connected if and only if it is path-connected and every loop at any basepoint is null-homotopic (i.e., homotopic to the constant loop).
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 144 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.
Cites18
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
- Pathstatement and proof · cited by 318
- Path.transproof · cited by 54
- Path.reflstatement and proof · cited by 36
- Path.symmproof · cited by 35
- Path.Homotopic.Quotient.mkproof · cited by 28
- Path.Homotopicstatement and proof · cited by 28
- PathConnectedSpacestatement and proof · cited by 26
- SimplyConnectedSpacestatement · cited by 19
- Path.Homotopic.setoidproof · cited by 14
- Path.Homotopic.Quotient.transproof · cited by 12
- Path.Homotopic.Quotient.reflproof · cited by 9
Cited by1
Results whose statement or proof uses this declaration.
- isSimplyConnected_iff_exists_homotopy_refl_forall_memproof · cited by 0