feat: port Topology.MetricSpace.HausdorffDistance (#3313)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib.lean

@@ -1725,6 +1725,7 @@ import Mathlib.Topology.MetricSpace.EMetricParacompact
 import Mathlib.Topology.MetricSpace.EMetricSpace
 import Mathlib.Topology.MetricSpace.Equicontinuity
 import Mathlib.Topology.MetricSpace.Gluing
+import Mathlib.Topology.MetricSpace.HausdorffDistance
 import Mathlib.Topology.MetricSpace.Infsep
 import Mathlib.Topology.MetricSpace.IsometricSMul
 import Mathlib.Topology.MetricSpace.Isometry

Mathlib/Data/Real/ENNReal.lean

@@ -694,6 +694,10 @@ theorem toReal_nat (n : ℕ) : (n : ℝ≥0∞).toReal = n := by
   rw [← ENNReal.ofReal_coe_nat n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)]
 #align ennreal.to_real_nat ENNReal.toReal_nat
 
+@[simp] theorem toReal_ofNat (n : ℕ) [n.AtLeastTwo] :
+    ENNReal.toReal (OfNat.ofNat n) = OfNat.ofNat n :=
+  toReal_nat n
+
 theorem le_coe_iff : a ≤ ↑r ↔ ∃ p : ℝ≥0, a = p ∧ p ≤ r := WithTop.le_coe_iff
 #align ennreal.le_coe_iff ENNReal.le_coe_iff
 
@@ -1940,6 +1944,12 @@ theorem toReal_mono (hb : b ≠ ∞) (h : a ≤ b) : a.toReal ≤ b.toReal :=
   (toReal_le_toReal (ne_top_of_le_ne_top hb h) hb).2 h
 #align ennreal.to_real_mono ENNReal.toReal_mono
 
+-- porting note: new lemma
+theorem toReal_mono' (h : a ≤ b) (ht : b = ∞ → a = ∞) : a.toReal ≤ b.toReal := by
+  rcases eq_or_ne a ∞ with rfl | ha
+  · exact toReal_nonneg
+  · exact toReal_mono (mt ht ha) h
+
 @[simp]
 theorem toReal_lt_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal < b.toReal ↔ a < b := by
   lift a to ℝ≥0 using ha
@@ -1951,10 +1961,27 @@ theorem toReal_strict_mono (hb : b ≠ ∞) (h : a < b) : a.toReal < b.toReal :=
   (toReal_lt_toReal h.ne_top hb).2 h
 #align ennreal.to_real_strict_mono ENNReal.toReal_strict_mono
 
-theorem toNNReal_mono (hb : b ≠ ∞) (h : a ≤ b) : a.toNNReal ≤ b.toNNReal := by
-  simpa [← ENNReal.coe_le_coe, hb, ne_top_of_le_ne_top hb h]
+theorem toNNReal_mono (hb : b ≠ ∞) (h : a ≤ b) : a.toNNReal ≤ b.toNNReal :=
+  toReal_mono hb h
 #align ennreal.to_nnreal_mono ENNReal.toNNReal_mono
 
+-- porting note: new lemma
+/-- If `a ≤ b + c` and `a = ∞` whenever `b = ∞` or `c = ∞`, then
+`ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c`. This lemma is useful to transfer
+triangle-like inequalities from `ENNReal`s to `Real`s. -/
+theorem toReal_le_add' (hle : a ≤ b + c) (hb : b = ∞ → a = ∞) (hc : c = ∞ → a = ∞) :
+    a.toReal ≤ b.toReal + c.toReal := by
+  refine le_trans (toReal_mono' hle ?_) toReal_add_le
+  simpa only [add_eq_top, or_imp] using And.intro hb hc
+
+-- porting note: new lemma
+/-- If `a ≤ b + c`, `b ≠ ∞`, and `c ≠ ∞`, then
+`ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c`. This lemma is useful to transfer
+triangle-like inequalities from `ENNReal`s to `Real`s. -/
+theorem toReal_le_add (hle : a ≤ b + c) (hb : b ≠ ∞) (hc : c ≠ ∞) :
+    a.toReal ≤ b.toReal + c.toReal :=
+  toReal_le_add' hle (flip absurd hb) (flip absurd hc)
+
 @[simp]
 theorem toNNReal_le_toNNReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toNNReal ≤ b.toNNReal ↔ a ≤ b :=
   ⟨fun h => by rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_le_coe], toNNReal_mono hb⟩

Mathlib/Mathport/Rename.lean

@@ -134,6 +134,7 @@ def suspiciousLean3Name (s : String) : Bool := Id.run do
   let allowed : List String :=
     ["Prop", "Type", "Pi", "Exists", "End",
      "Inf", "Sup", "Union", "Inter",
+     "Hausdorff",
      "Ioo", "Ico", "Iio", "Icc", "Iic", "Ioc", "Ici", "Ioi", "Ixx"]
   let mut s := s
   for a in allowed do

Mathlib/Topology/MetricSpace/Basic.lean

@@ -1282,8 +1282,7 @@ def PseudoEMetricSpace.toPseudoMetricSpaceOfDist {α : Type u} [e : PseudoEMetri
   dist_comm x y := by simp [h, edist_comm]
   dist_triangle x y z := by
     simp only [h]
-    exact (ENNReal.toReal_mono (ENNReal.add_ne_top.2 ⟨edist_ne_top _ _, edist_ne_top _ _⟩)
-      (edist_triangle _ _ _)).trans ENNReal.toReal_add_le
+    exact ENNReal.toReal_le_add (edist_triangle _ _ _) (edist_ne_top _ _) (edist_ne_top _ _)
   edist := edist
   edist_dist _ _ := by simp only [h, ENNReal.ofReal_toReal (edist_ne_top _ _)]
   toUniformSpace := e.toUniformSpace
@@ -2648,6 +2647,9 @@ theorem Bounded.ediam_ne_top (h : Bounded s) : EMetric.diam s ≠ ⊤ :=
   bounded_iff_ediam_ne_top.1 h
 #align metric.bounded.ediam_ne_top Metric.Bounded.ediam_ne_top
 
+theorem ediam_eq_top_iff_unbounded : EMetric.diam s = ⊤ ↔ ¬Bounded s :=
+  bounded_iff_ediam_ne_top.not_left.symm
+
 theorem ediam_univ_eq_top_iff_noncompact [ProperSpace α] :
     EMetric.diam (univ : Set α) = ∞ ↔ NoncompactSpace α := by
   rw [← not_compactSpace_iff, compactSpace_iff_bounded_univ, bounded_iff_ediam_ne_top,
@@ -2670,8 +2672,7 @@ theorem dist_le_diam_of_mem (h : Bounded s) (hx : x ∈ s) (hy : y ∈ s) : dist
   dist_le_diam_of_mem' h.ediam_ne_top hx hy
 #align metric.dist_le_diam_of_mem Metric.dist_le_diam_of_mem
 
-theorem ediam_of_unbounded (h : ¬Bounded s) : EMetric.diam s = ∞ := by
-  rwa [bounded_iff_ediam_ne_top, Classical.not_not] at h
+theorem ediam_of_unbounded (h : ¬Bounded s) : EMetric.diam s = ∞ := ediam_eq_top_iff_unbounded.2 h
 #align metric.ediam_of_unbounded Metric.ediam_of_unbounded
 
 /-- An unbounded set has zero diameter. If you would prefer to get the value ∞, use `EMetric.diam`.
@@ -2690,15 +2691,12 @@ any two points in each of the sets. This lemma is true without any side conditio
 obviously true if `s ∪ t` is unbounded. -/
 theorem diam_union {t : Set α} (xs : x ∈ s) (yt : y ∈ t) :
     diam (s ∪ t) ≤ diam s + dist x y + diam t := by
-  by_cases H : Bounded (s ∪ t)
-  · have hs : Bounded s := H.mono (subset_union_left _ _)
-    have ht : Bounded t := H.mono (subset_union_right _ _)
-    rw [bounded_iff_ediam_ne_top] at H hs ht
-    rw [dist_edist, diam, diam, diam, ← ENNReal.toReal_add, ← ENNReal.toReal_add,
-      ENNReal.toReal_le_toReal] <;> apply_rules [ENNReal.add_ne_top.2, And.intro, edist_ne_top]
-    exact EMetric.diam_union xs yt
-  · rw [diam_eq_zero_of_unbounded H]
-    apply_rules [add_nonneg, diam_nonneg, dist_nonneg]
+  simp only [diam, dist_edist]
+  refine (ENNReal.toReal_le_add' (EMetric.diam_union xs yt) ?_ ?_).trans
+    (add_le_add_right ENNReal.toReal_add_le _)
+  · simp only [ENNReal.add_eq_top, edist_ne_top, or_false]
+    exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono (subset_union_left _ _)
+  · exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono (subset_union_right _ _)
 #align metric.diam_union Metric.diam_union
 
 /-- If two sets intersect, the diameter of the union is bounded by the sum of the diameters. -/