Commit 2024-01-08 16:08 87fc4077

View on Github →

chore(LocallyCompact): rename the "of basis" constructor (#9327) Rename locallyCompactSpace_of_hasBasis to LocallyCompactSpace.of_hasBasis to allow the new-style dot notation.

Estimated changes

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

added theorem LocallyCompactSpace.of_hasBasis

deleted theorem locallyCompactSpace_of_hasBasis

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean