Commit 2023-07-07 13:47 38b0bb05

View on Github →

feat: port AlgebraicTopology.FundamentalGroupoid.SimplyConnected (#5759)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean

added theorem SimplyConnectedSpace.paths_homotopic

added theorem simply_connected_def

added theorem simply_connected_iff_paths_homotopic'

added theorem simply_connected_iff_paths_homotopic

added theorem simply_connected_iff_unique_homotopic