Commit 2025-07-05 13:07 063d2e5d

chore(Topology/LiminfLimsup): split out non-algebraic content from Topology/Algebra file (#26560) All the moved content had no algebraic material (in particular required no algebraic imports), so we move it out of Topology/Algebra. This increases discoverability and improves the global organisation of Topology/, and gives a net import decrease across mathlib.