Commit 2024-10-18 05:56 5d0c5274

View on Github →

feat(PathConnected): review API, add missing lemmas (#17855)

Estimated changes

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

Modified Mathlib/Analysis/Convex/Normed.lean

Modified Mathlib/Topology/Connected/PathConnected.lean

added theorem Inducing.joinedIn_image

modified theorem IsOpen.isConnected_iff_isPathConnected

added theorem IsOpen.locPathConnectedSpace

modified theorem IsPathConnected.image

added theorem JoinedIn.map

added theorem JoinedIn.map_continuousOn

added theorem LocPathConnectedSpace.of_bases

added theorem OpenEmbedding.locPathConnectedSpace

deleted theorem locPathConnected_of_bases

deleted theorem locPathConnected_of_isOpen

added theorem mem_pathComponent_iff

added theorem pathComponent_eq_connectedComponent

modified theorem pathConnectedSpace_iff_connectedSpace

modified theorem pathConnected_subset_basis