completely pseudometrizable

Author: CoolRmal

Mathlib/Topology/Baire/CompleteMetrizable.lean

@@ -4,28 +4,22 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Yury Kudryashov
 -/
 import Mathlib.Analysis.SpecificLimits.Basic
-import Mathlib.Tactic.Finiteness
-import Mathlib.Topology.Metrizable.Uniformity
+import Mathlib.Topology.Metrizable.CompletelyMetrizable
 
 /-!
 # First Baire theorem
 
-In this file we prove that a completely metrizable topological space is a Baire space.
-Since `Mathlib` does not have the notion of a completely metrizable topological space yet,
-we state it for a complete uniform space with countably generated uniformity filter.
+In this file we prove that a completely pseudometrizable topological space is a Baire space.
 -/
 
-open Filter EMetric Set
-open scoped Topology Uniformity ENNReal
+open EMetric Set TopologicalSpace
+open scoped ENNReal
 
-variable {X : Type*} [UniformSpace X] [CompleteSpace X] [(𝓤 X).IsCountablyGenerated]
+variable {X : Type*} [TopologicalSpace X] [IsCompletelyPseudoMetrizableSpace X]
 
-/-- **First Baire theorem**: a completely metrizable topological space has Baire property.
-
-Since `Mathlib` does not have the notion of a completely metrizable topological space yet,
-we state it for a complete uniform space with countably generated uniformity filter. -/
-instance (priority := 100) BaireSpace.of_pseudoEMetricSpace_completeSpace : BaireSpace X := by
-  let _ := UniformSpace.pseudoMetricSpace X
+/-- **First Baire theorem**: a completely pseudometrizable topological space has Baire property. -/
+instance (priority := 100) BaireSpace.of_pseudoMetricSpace_completeSpace : BaireSpace X := by
+  let _ := upgradeIsCompletelyPseudoMetrizable X
   refine ⟨fun f ho hd => ?_⟩
   let B : ℕ → ℝ≥0∞ := fun n => 1 / 2 ^ n
   have Bpos : ∀ n, 0 < B n := fun n ↦

Mathlib/Topology/Metrizable/CompletelyMetrizable.lean

@@ -7,27 +7,29 @@ import Mathlib.Topology.MetricSpace.Gluing
 import Mathlib.Topology.Metrizable.Uniformity
 
 /-!
-# Completely metrizable spaces
+# Completely (pseudo)metrizable spaces
 
-A topological space is completely metrizable if one can endow it with a `MetricSpace` structure
-which makes it complete and gives the same topology. This typeclass allows to state theorems
-which do not require a `MetricSpace` structure to make sense without introducing such a structure.
+A topological space is completely (pseudo)metrizable if one can endow it with a
+`(Pseudo)MetricSpace` structure which makes it complete and gives the same topology. This typeclass
+allows to state theorems which do not require a `(Pseudo)MetricSpace` structure to make sense
+without introducing such a structure.
 It is in particular useful in measure theory, where one often assumes that a space is a
 `PolishSpace`, i.e. a separable and completely metrizable space. Sometimes the separability
 hypothesis is not needed and the right assumption is then `IsCompletelyMetrizableSpace`.
 
 ## Main definition
 
-* `IsCompletelyMetrizableSpace X`: A topological space is completely metrizable if there exists a
-  metric space structure compatible with the topology which makes the space complete.
-  To endow such a space with a compatible distance, use `letI := upgradeIsCompletelyMetrizable X`.
+* `IsCompletely(Pseudo)MetrizableSpace X`: A topological space is completely (pseudo)metrizable if
+  there exists a (pseudo)metric space structure compatible with the topology which makes the space
+  complete. To endow such a space with a compatible distance, use
+  `letI := upgradeIsCompletely(Pseudo)Metrizable X`.
 
 ## Implementation note
 
-Given a `IsCompletelyMetrizableSpace X` instance, one may want to endow `X` with a complete metric.
-This can be done by writing `letI := upgradeIsCompletelyMetrizable X`, which will endow `X` with
-an `UpgradedIsCompletelyMetrizableSpace X` instance. This class is a convenience class and
-no instance should be registered for it.
+Given a `IsCompletely(Pseudo)MetrizableSpace X` instance, one may want to endow `X` with a complete
+(pseudo)metric. This can be done by writing `letI := upgradeIsCompletely(Pseudo)Metrizable X`,
+which will endow `X` with an `UpgradedIsCompletely(Pseudo)MetrizableSpace X` instance. This class
+is a convenience class and no instance should be registered for it.
 -/
 
 open Filter Function Set Topology
@@ -36,6 +38,52 @@ variable {X Y : Type*}
 
 namespace TopologicalSpace
 
+/-- A topological space is completely pseudometrizable if there exists a pseudometric space
+structure compatible with the topology which makes the space complete.
+To endow such a space with a compatible distance, use
+`letI := upgradeIsCompletelyPseudoMetrizable X`. -/
+class IsCompletelyPseudoMetrizableSpace (X : Type*) [t : TopologicalSpace X] : Prop where
+  complete : ∃ m : PseudoMetricSpace X, m.toUniformSpace.toTopologicalSpace = t ∧
+    @CompleteSpace X m.toUniformSpace
+
+instance (priority := 100) _root_.PseudoMetricSpace.toIsCompletelPseudoMetrizableSpace
+    [PseudoMetricSpace X] [CompleteSpace X] : IsCompletelyPseudoMetrizableSpace X :=
+  ⟨⟨‹_›, rfl, ‹_›⟩⟩
+
+/-- A convenience class, for a completely pseudometrizable space endowed with a complete
+pseudometric. No instance of this class should be registered: It should be used as
+`letI := upgradeIsCompletelyPseudoMetrizable X` to endow a completely pseudometrizable
+space with a complete pseudometric. -/
+class UpgradedIsCompletelyPseudoMetrizableSpace (X : Type*) extends
+  PseudoMetricSpace X, CompleteSpace X
+
+open scoped Uniformity in
+instance (priority := 100) IsCompletelyPseudoMetrizableSpace.of_completeSpace_pseudometrizable
+    [UniformSpace X] [CompleteSpace X] [(𝓤 X).IsCountablyGenerated] :
+    IsCompletelyPseudoMetrizableSpace X where
+  complete := ⟨UniformSpace.pseudoMetricSpace X, rfl, ‹_›⟩
+
+/-- Construct on a completely pseudometrizable space a pseudometric (compatible with the topology)
+which is complete. -/
+noncomputable def completelyPseudoMetrizableMetric (X : Type*) [TopologicalSpace X]
+    [h : IsCompletelyPseudoMetrizableSpace X] : PseudoMetricSpace X :=
+  h.complete.choose.replaceTopology h.complete.choose_spec.1.symm
+
+theorem complete_completelyPseudoMetrizableMetric (X : Type*) [ht : TopologicalSpace X]
+    [h : IsCompletelyPseudoMetrizableSpace X] :
+    @CompleteSpace X (completelyPseudoMetrizableMetric X).toUniformSpace := by
+  convert h.complete.choose_spec.2
+  exact PseudoMetricSpace.replaceTopology_eq _ _
+
+/-- This definition endows a completely pseudometrizable space with a complete pseudometric.
+Use it as: `letI := upgradeIsCompletelyMetrizable X`. -/
+noncomputable
+def upgradeIsCompletelyPseudoMetrizable (X : Type*) [TopologicalSpace X]
+    [IsCompletelyPseudoMetrizableSpace X] :
+    UpgradedIsCompletelyPseudoMetrizableSpace X :=
+  letI := completelyPseudoMetrizableMetric X
+  { complete_completelyPseudoMetrizableMetric X with }
+
 /-- A topological space is completely metrizable if there exists a metric space structure
 compatible with the topology which makes the space complete.
 To endow such a space with a compatible distance, use
@@ -44,6 +92,12 @@ class IsCompletelyMetrizableSpace (X : Type*) [t : TopologicalSpace X] : Prop wh
   complete : ∃ m : MetricSpace X, m.toUniformSpace.toTopologicalSpace = t ∧
     @CompleteSpace X m.toUniformSpace
 
+/-- A completely metrizable space is completely pseudometrizable. -/
+instance IsCompletelyPseudoMetrizableSpace.IsCompletelyMetrizableSpace [TopologicalSpace X]
+    [IsCompletelyMetrizableSpace X] : IsCompletelyPseudoMetrizableSpace X := by
+  obtain ⟨m, _, _⟩ := ‹_›
+  use m.toPseudoMetricSpace
+
 instance (priority := 100) _root_.MetricSpace.toIsCompletelyMetrizableSpace
     [MetricSpace X] [CompleteSpace X] : IsCompletelyMetrizableSpace X :=
   ⟨⟨‹_›, rfl, ‹_›⟩⟩