feat: port Topology.MetricSpace.Polish (#3357)

Co-authored-by: Scott Morrison <scott@tqft.net>

Author: urkud

Mathlib.lean

@@ -1884,6 +1884,7 @@ import Mathlib.Topology.MetricSpace.Isometry
 import Mathlib.Topology.MetricSpace.Lipschitz
 import Mathlib.Topology.MetricSpace.MetricSeparated
 import Mathlib.Topology.MetricSpace.PiNat
+import Mathlib.Topology.MetricSpace.Polish
 import Mathlib.Topology.MetricSpace.ShrinkingLemma
 import Mathlib.Topology.NhdsSet
 import Mathlib.Topology.NoetherianSpace

Mathlib/Topology/Constructions.lean

@@ -1395,19 +1395,21 @@ theorem pi_generateFrom_eq_finite {π : ι → Type _} {g : ∀ a, Set (Set (π
     by_cases a ∈ i <;> simp [*]
 #align pi_generate_from_eq_finite pi_generateFrom_eq_finite
 
+-- porting note: new lemma
+theorem induced_to_pi {X : Type _} (f : X → ∀ i, π i) :
+    induced f Pi.topologicalSpace = ⨅ i, induced (f · i) inferInstance := by
+  erw [induced_infᵢ]
+  simp only [induced_compose]
+  rfl
+
 /-- Suppose `π i` is a family of topological spaces indexed by `i : ι`, and `X` is a type
 endowed with a family of maps `f i : X → π i` for every `i : ι`, hence inducing a
 map `g : X → Π i, π i`. This lemma shows that infimum of the topologies on `X` induced by
 the `f i` as `i : ι` varies is simply the topology on `X` induced by `g : X → Π i, π i`
 where `Π i, π i` is endowed with the usual product topology. -/
 theorem inducing_infᵢ_to_pi {X : Type _} (f : ∀ i, X → π i) :
-    @Inducing X (∀ i, π i) (⨅ i, induced (f i) inferInstance) _ fun x i => f i x := by
-  letI := ⨅ i, induced (f i) inferInstance
-  constructor
-  erw [induced_infᵢ]
-  congr 1
-  funext
-  erw [induced_compose]; rfl
+    @Inducing X (∀ i, π i) (⨅ i, induced (f i) inferInstance) _ fun x i => f i x :=
+  letI := ⨅ i, induced (f i) inferInstance; ⟨(induced_to_pi _).symm⟩
 #align inducing_infi_to_pi inducing_infᵢ_to_pi
 
 variable [Finite ι] [∀ i, DiscreteTopology (π i)]

Mathlib/Topology/MetricSpace/HausdorffDistance.lean

@@ -591,6 +591,14 @@ theorem _root_.IsClosed.not_mem_iff_infDist_pos (h : IsClosed s) (hs : s.Nonempt
   simp [h.mem_iff_infDist_zero hs, infDist_nonneg.gt_iff_ne]
 #align is_closed.not_mem_iff_inf_dist_pos IsClosed.not_mem_iff_infDist_pos
 
+-- porting note: new lemma
+theorem continuousAt_inv_infDist_pt (h : x ∉ closure s) :
+    ContinuousAt (fun x ↦ (infDist x s)⁻¹) x := by
+  rcases s.eq_empty_or_nonempty with (rfl | hs)
+  · simp only [infDist_empty, continuousAt_const]
+  · refine (continuous_infDist_pt s).continuousAt.inv₀ ?_
+    rwa [Ne.def, ← mem_closure_iff_infDist_zero hs]
+
 /-- The infimum distance is invariant under isometries -/
 theorem infDist_image (hΦ : Isometry Φ) : infDist (Φ x) (Φ '' t) = infDist x t := by
   simp [infDist, infEdist_image hΦ]