Commit 2026-01-12 10:37 0c756a21

View on Github →

feat(FundamentalGroupoid): define simply connected sets (#33447)

Estimated changes

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean

added theorem ContinuousMap.HomotopyEquiv.simplyConnectedSpace

added theorem ContinuousMap.HomotopyEquiv.simplyConnectedSpace_iff

added theorem Homeomorph.isSimplyConnected_image

added theorem Homeomorph.isSimplyConnected_preimage

added theorem IsSimplyConnected.isPathConnected

added theorem IsSimplyConnected.nonempty

added theorem IsSimplyConnected.simplyConnectedSpace

added def IsSimplyConnected

added theorem Topology.IsEmbedding.isSimplyConnected_image

added theorem isSimplyConnected_iff_exists_homotopy_refl_forall_mem

added theorem isSimplyConnected_smul_set_iff

added theorem isSimplyConnected_smul_set₀_iff

modified theorem simply_connected_iff_loops_nullhomotopic

modified theorem simply_connected_iff_paths_homotopic'

modified theorem simply_connected_iff_paths_homotopic

Modified Mathlib/Topology/Connected/PathConnected.lean

added theorem IsPathConnected.nonempty