Commit 2025-02-09 22:27 15986855

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 of Mathlib.Topology.Connected.LocPathConnected, as about half the contents of that file are from an earlier PR of mine.