Update CompletelyMetrizable.lean

CoolRmal · CoolRmal · commit 3bc520d8ffbe · 2025-11-04T18:38:03.000-05:00
diff --git a/Mathlib/Topology/Metrizable/CompletelyMetrizable.lean b/Mathlib/Topology/Metrizable/CompletelyMetrizable.lean
@@ -76,7 +76,7 @@ theorem complete_completelyPseudoMetrizableMetric (X : Type*) [ht : TopologicalS
   exact PseudoMetricSpace.replaceTopology_eq _ _
 
 /-- This definition endows a completely pseudometrizable space with a complete pseudometric.
-Use it as: `letI := upgradeIsCompletelyMetrizable X`. -/
+Use it as: `letI := upgradeIsCompletelyPseudoMetrizable X`. -/
 noncomputable
 def upgradeIsCompletelyPseudoMetrizable (X : Type*) [TopologicalSpace X]
     [IsCompletelyPseudoMetrizableSpace X] :
