Commit 2023-08-04 10:00 d2b1b371

View on Github →

feat: complements on connectedness and path-connectedness (#6347)

Estimated changes

Modified Mathlib/Topology/Connected.lean

added theorem IsPreconnected.induction₂'

added theorem IsPreconnected.induction₂

added theorem PreconnectedSpace.induction₂'

added theorem PreconnectedSpace.induction₂

Modified Mathlib/Topology/PathConnected.lean

added theorem IsPathConnected.image'

added def Path.map'

added theorem isPathConnected_singleton