Commit 2025-12-11 17:07 32831aa9

View on Github →

doc(Topology): fix typos (#32659) Typos found and fixed by Codex.

Estimated changes

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

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/EMetricSpace/PairReduction.lean

Modified Mathlib/Topology/Homotopy/HSpaces.lean

Modified Mathlib/Topology/MetricSpace/Bounded.lean

Modified Mathlib/Topology/MetricSpace/Gluing.lean

Modified Mathlib/Topology/MetricSpace/PiNat.lean

Modified Mathlib/Topology/MetricSpace/ProperSpace.lean

Modified Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

Modified Mathlib/Topology/Metrizable/Basic.lean

Modified Mathlib/Topology/Metrizable/Uniformity.lean

Modified Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean

Modified Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean

Modified Mathlib/Topology/UniformSpace/AbstractCompletion.lean