Theorem simply_connected_iff_loops_nullhomotopic

Modification history

2026-01-12 10:37
Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean
feat(FundamentalGroupoid): define simply connected sets (#33447)
Modified simply_connected_iff_loops_nullhomotopicView on Github →
2025-11-30 19:57
Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean
feat: alternative characterisation of SimplyConnectedSpace (#31737) …
Added simply_connected_iff_loops_nullhomotopicView on Github →