chore(topology/metric_space/hausdorff_distance): move two lemmas (#12771)

Remove the dependence of `topology/metric_space/hausdorff_distance` on `analysis.normed_space.basic`, by moving out two lemmas.

Author: hrmacbeth

src/analysis/normed_space/finite_dimension.lean

@@ -3,9 +3,10 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
+import analysis.asymptotics.asymptotic_equivalent
 import analysis.normed_space.affine_isometry
 import analysis.normed_space.operator_norm
-import analysis.asymptotics.asymptotic_equivalent
+import analysis.normed_space.riesz_lemma
 import linear_algebra.matrix.to_lin
 import topology.algebra.matrix
 

src/analysis/normed_space/riesz_lemma.lean

@@ -1,21 +1,28 @@
 /-
 Copyright (c) 2019 Jean Lo. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jean Lo
+Authors: Jean Lo, Yury Kudryashov
 -/
+import analysis.normed_space.basic
 import topology.metric_space.hausdorff_distance
 
 /-!
-# Riesz's lemma
+# Applications of the Hausdorff distance in normed spaces
 
 Riesz's lemma, stated for a normed space over a normed field: for any
 closed proper subspace `F` of `E`, there is a nonzero `x` such that `∥x - F∥`
 is at least `r * ∥x∥` for any `r < 1`. This is `riesz_lemma`.
 
 In a nondiscrete normed field (with an element `c` of norm `> 1`) and any `R > ∥c∥`, one can
 guarantee `∥x∥ ≤ R` and `∥x - y∥ ≥ 1` for any `y` in `F`. This is `riesz_lemma_of_norm_lt`.
+
+A further lemma, `closed_ball_inf_dist_compl_subset_closure`, finds a *closed* ball within the
+closure of a set `s` of optimal distance from a point in `x` to the frontier of `s`.
 -/
 
+open set metric
+open_locale topological_space
+
 variables {𝕜 : Type*} [normed_field 𝕜]
 variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
 
@@ -89,3 +96,28 @@ begin
     mul_le_mul_of_nonneg_left (hx y' (by simp [hy', submodule.smul_mem _ _ hy])) (norm_nonneg _)
   ... = ∥d • x - y∥ : by simp [yy', ← smul_sub, norm_smul],
 end
+
+lemma metric.closed_ball_inf_dist_compl_subset_closure' {E : Type*} [semi_normed_group E]
+  [normed_space ℝ E] {x : E} {s : set E} (hx : s ∈ 𝓝 x) (hs : s ≠ univ) :
+  closed_ball x (inf_dist x sᶜ) ⊆ closure s :=
+begin
+  have hne : sᶜ.nonempty, from nonempty_compl.2 hs,
+  have hpos : 0 < inf_dist x sᶜ,
+  { rwa [← inf_dist_eq_closure, ← is_closed_closure.not_mem_iff_inf_dist_pos hne.closure,
+      closure_compl, mem_compl_iff, not_not, mem_interior_iff_mem_nhds] },
+  rw ← closure_ball x hpos,
+  apply closure_mono,
+  rw [← le_eq_subset, ← is_compl_compl.disjoint_right_iff],
+  exact disjoint_ball_inf_dist
+end
+
+lemma metric.closed_ball_inf_dist_compl_subset_closure [normed_space ℝ E]
+  {x : E} {s : set E} (hx : x ∈ s) (hs : s ≠ univ) :
+  closed_ball x (inf_dist x sᶜ) ⊆ closure s :=
+begin
+  by_cases hx' : x ∈ closure sᶜ,
+  { rw [mem_closure_iff_inf_dist_zero (nonempty_compl.2 hs)] at hx',
+    simpa [hx'] using subset_closure hx },
+  { rw [closure_compl, mem_compl_iff, not_not, mem_interior_iff_mem_nhds] at hx',
+    exact metric.closed_ball_inf_dist_compl_subset_closure' hx' hs }
+end

src/topology/metric_space/hausdorff_distance.lean

@@ -3,7 +3,6 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import analysis.normed_space.basic
 import analysis.specific_limits.basic
 import topology.metric_space.isometry
 import topology.instances.ennreal
@@ -540,31 +539,6 @@ lemma exists_mem_closure_inf_dist_eq_dist [proper_space α] (hne : s.nonempty) (
   ∃ y ∈ closure s, inf_dist x s = dist x y :=
 by simpa only [inf_dist_eq_closure] using is_closed_closure.exists_inf_dist_eq_dist hne.closure x
 
-lemma closed_ball_inf_dist_compl_subset_closure' {E : Type*} [semi_normed_group E]
-  [normed_space ℝ E] {x : E} {s : set E} (hx : s ∈ 𝓝 x) (hs : s ≠ univ) :
-  closed_ball x (inf_dist x sᶜ) ⊆ closure s :=
-begin
-  have hne : sᶜ.nonempty, from nonempty_compl.2 hs,
-  have hpos : 0 < inf_dist x sᶜ,
-  { rwa [← inf_dist_eq_closure, ← is_closed_closure.not_mem_iff_inf_dist_pos hne.closure,
-      closure_compl, mem_compl_iff, not_not, mem_interior_iff_mem_nhds] },
-  rw ← closure_ball x hpos,
-  apply closure_mono,
-  rw [← le_eq_subset, ← is_compl_compl.disjoint_right_iff],
-  exact disjoint_ball_inf_dist
-end
-
-lemma closed_ball_inf_dist_compl_subset_closure {E : Type*} [normed_group E] [normed_space ℝ E]
-  {x : E} {s : set E} (hx : x ∈ s) (hs : s ≠ univ) :
-  closed_ball x (inf_dist x sᶜ) ⊆ closure s :=
-begin
-  by_cases hx' : x ∈ closure sᶜ,
-  { rw [mem_closure_iff_inf_dist_zero (nonempty_compl.2 hs)] at hx',
-    simpa [hx'] using subset_closure hx },
-  { rw [closure_compl, mem_compl_iff, not_not, mem_interior_iff_mem_nhds] at hx',
-    exact closed_ball_inf_dist_compl_subset_closure' hx' hs }
-end
-
 /-! ### Distance of a point to a set as a function into `ℝ≥0`. -/
 
 /-- The minimal distance of a point to a set as a `ℝ≥0` -/

src/topology/metric_space/pi_nat.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
+import tactic.ring_exp
 import topology.metric_space.hausdorff_distance
 
 /-!

src/topology/metric_space/polish.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
+import analysis.normed_space.basic
 import topology.metric_space.pi_nat
 import topology.metric_space.isometry
 import topology.metric_space.gluing
@@ -19,7 +20,7 @@ In this file, we establish the basic properties of Polish spaces.
 * `polish_space α` is a mixin typeclass on a topological space, requiring that the topology is
   second-countable and compatible with a complete metric. To endow the space with such a metric,
   use in a proof `letI := upgrade_polish_space α`.
-  We register an instance from complete second-countable metric spaces to polish spaces, not the
+  We register an instance from complete second-countable metric spaces to Polish spaces, not the
   other way around.
 * We register that countable products and sums of Polish spaces are Polish.
 * `is_closed.polish_space`: a closed subset of a Polish space is Polish.