Commit 2025-12-22 13:19 8a100fb2

View on Github →

chore(Topology): fix whitespace (#33164) Found by extending the commandStart linter to proof bodies.

Estimated changes

Modified Mathlib/Topology/Algebra/InfiniteSum/Group.lean

Modified Mathlib/Topology/Algebra/Module/Cardinality.lean

Modified Mathlib/Topology/Algebra/UniformField.lean

Modified Mathlib/Topology/Category/CompactlyGenerated.lean

Modified Mathlib/Topology/Category/LightProfinite/Basic.lean

modified structure LightDiagram

Modified Mathlib/Topology/Category/Sequential.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean

Modified Mathlib/Topology/EMetricSpace/Lipschitz.lean

Modified Mathlib/Topology/Instances/CantorSet.lean

Modified Mathlib/Topology/MetricSpace/Contracting.lean

Modified Mathlib/Topology/MetricSpace/Gluing.lean

Modified Mathlib/Topology/MetricSpace/HausdorffAlexandroff.lean

Modified Mathlib/Topology/MetricSpace/Lipschitz.lean

Modified Mathlib/Topology/NoetherianSpace.lean

Modified Mathlib/Topology/Order/LeftRightNhds.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean

Modified Mathlib/Topology/UniformSpace/HeineCantor.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

Modified Mathlib/Topology/UnitInterval.lean