Commit 2025-02-09 22:27 15986855
View on Github →chore(Topology/Connected): split PathConnected.lean
(#21591)
Splits Mathlib.Topology.Connected.PathConnected
into three files:
Mathlib.Topology.Path
, which now contains the basic API for paths,Mathlib.Topology.Connected.PathConnected
, which retains the work on path components and path-connected sets and spaces,Mathlib.Topology.Connected.LocPathConnected
, which now contains everything relating to locally path-connected spaces. While splitting this file I have also taken the liberty to insert my name into the authors list ofMathlib.Topology.Connected.LocPathConnected
, as about half the contents of that file are from an earlier PR of mine.