Commit 2025-06-10 20:04 8b578dd9

View on Github →

feat: add path component of the identity in a locally path connected topological group, as an open normal subgroup (#25668)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Connected/PathComponentOne.lean

added def OpenNormalSubgroup.pathComponentOne

Modified Mathlib/Topology/Connected/PathConnected.lean

added theorem IsPathConnected.inv

added theorem Joined.inv

added theorem Joined.listProd

added theorem JoinedIn.inv

added def Subgroup.pathComponentOne

added def Submonoid.pathComponentOne

Modified Mathlib/Topology/Path.lean

added def Path.inv