Theorem isSimplyConnected_iff_exists_homotopy_refl_forall_mem

Modification history

2026-01-12 10:37
Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean
feat(FundamentalGroupoid): define simply connected sets (#33447)
Added isSimplyConnected_iff_exists_homotopy_refl_forall_memView on Github →