[Merged by Bors] - chore: splitting up metric spaces files

Mathlib.lean

@@ -4433,6 +4433,8 @@ import Mathlib.Topology.DerivedSet
 import Mathlib.Topology.DiscreteQuotient
 import Mathlib.Topology.DiscreteSubset
 import Mathlib.Topology.EMetricSpace.Basic
+import Mathlib.Topology.EMetricSpace.Defs
+import Mathlib.Topology.EMetricSpace.Diam
 import Mathlib.Topology.EMetricSpace.Lipschitz
 import Mathlib.Topology.EMetricSpace.Paracompact
 import Mathlib.Topology.ExtendFrom
@@ -4498,6 +4500,7 @@ import Mathlib.Topology.MetricSpace.Cauchy
 import Mathlib.Topology.MetricSpace.Closeds
 import Mathlib.Topology.MetricSpace.Completion
 import Mathlib.Topology.MetricSpace.Contracting
+import Mathlib.Topology.MetricSpace.Defs
 import Mathlib.Topology.MetricSpace.Dilation
 import Mathlib.Topology.MetricSpace.DilationEquiv
 import Mathlib.Topology.MetricSpace.Equicontinuity
@@ -4519,9 +4522,12 @@ import Mathlib.Topology.MetricSpace.PiNat
 import Mathlib.Topology.MetricSpace.Polish
 import Mathlib.Topology.MetricSpace.ProperSpace
 import Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
+import Mathlib.Topology.MetricSpace.Pseudo.Basic
 import Mathlib.Topology.MetricSpace.Pseudo.Constructions
 import Mathlib.Topology.MetricSpace.Pseudo.Defs
 import Mathlib.Topology.MetricSpace.Pseudo.Lemmas
+import Mathlib.Topology.MetricSpace.Pseudo.Pi
+import Mathlib.Topology.MetricSpace.Pseudo.Real
 import Mathlib.Topology.MetricSpace.Sequences
 import Mathlib.Topology.MetricSpace.ShrinkingLemma
 import Mathlib.Topology.MetricSpace.ThickenedIndicator

Mathlib/Analysis/BoxIntegral/Box/Basic.lean

@@ -8,7 +8,7 @@ import Mathlib.Order.Interval.Set.Monotone
 import Mathlib.Topology.MetricSpace.Basic
 import Mathlib.Topology.MetricSpace.Bounded
 import Mathlib.Topology.Order.MonotoneConvergence
-import Mathlib.Topology.MetricSpace.Pseudo.Lemmas
+import Mathlib.Topology.MetricSpace.Pseudo.Real
 /-!
 # Rectangular boxes in `ℝⁿ`
 

Mathlib/Analysis/Convex/Extrema.lean

@@ -5,8 +5,8 @@ Authors: Frédéric Dupuis
 -/
 import Mathlib.Analysis.Convex.Function
 import Mathlib.Topology.Algebra.Affine
-import Mathlib.Topology.MetricSpace.Pseudo.Lemmas
 import Mathlib.Topology.Order.LocalExtr
+import Mathlib.Topology.MetricSpace.Pseudo.Lemmas
 
 /-!
 # Minima and maxima of convex functions

Mathlib/Analysis/Oscillation.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 James Sundstrom. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: James Sundstrom
 -/
-import Mathlib.Topology.EMetricSpace.Basic
+import Mathlib.Topology.EMetricSpace.Diam
 import Mathlib.Order.WellFoundedSet
 
 /-!

Mathlib/InformationTheory/Hamming.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wrenna Robson
 -/
 import Mathlib.Analysis.Normed.Group.Basic
-import Mathlib.Topology.Instances.Discrete
 
 /-!
 # Hamming spaces

Mathlib/Topology/EMetricSpace/Diam.lean

@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2015, 2017 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébastien Gouëzel
+-/
+import Mathlib.Topology.EMetricSpace.Basic
+import Mathlib.Data.ENNReal.Real
+
+/-!
+# Diameters of sets in extended metric spaces
+
+-/
+
+
+open Set Filter Classical
+
+open scoped Uniformity Topology Filter NNReal ENNReal Pointwise
+
+universe u v w
+
+variable {α β : Type*} {s : Set α} {x y z : α}
+
+namespace EMetric
+
+section
+variable [PseudoEMetricSpace α]
+
+/-- The diameter of a set in a pseudoemetric space, named `EMetric.diam` -/
+noncomputable def diam (s : Set α) :=
+  ⨆ (x ∈ s) (y ∈ s), edist x y
+
+theorem diam_eq_sSup (s : Set α) : diam s = sSup (image2 edist s s) := sSup_image2.symm
+
+theorem diam_le_iff {d : ℝ≥0∞} : diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d := by
+  simp only [diam, iSup_le_iff]
+
+theorem diam_image_le_iff {d : ℝ≥0∞} {f : β → α} {s : Set β} :
+    diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d := by
+  simp only [diam_le_iff, forall_mem_image]
+
+theorem edist_le_of_diam_le {d} (hx : x ∈ s) (hy : y ∈ s) (hd : diam s ≤ d) : edist x y ≤ d :=
+  diam_le_iff.1 hd x hx y hy
+
+/-- If two points belong to some set, their edistance is bounded by the diameter of the set -/
+theorem edist_le_diam_of_mem (hx : x ∈ s) (hy : y ∈ s) : edist x y ≤ diam s :=
+  edist_le_of_diam_le hx hy le_rfl
+
+/-- If the distance between any two points in a set is bounded by some constant, this constant
+bounds the diameter. -/
+theorem diam_le {d : ℝ≥0∞} (h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) : diam s ≤ d :=
+  diam_le_iff.2 h
+
+/-- The diameter of a subsingleton vanishes. -/
+theorem diam_subsingleton (hs : s.Subsingleton) : diam s = 0 :=
+  nonpos_iff_eq_zero.1 <| diam_le fun _x hx y hy => (hs hx hy).symm ▸ edist_self y ▸ le_rfl
+
+/-- The diameter of the empty set vanishes -/
+@[simp]
+theorem diam_empty : diam (∅ : Set α) = 0 :=
+  diam_subsingleton subsingleton_empty
+
+/-- The diameter of a singleton vanishes -/
+@[simp]
+theorem diam_singleton : diam ({x} : Set α) = 0 :=
+  diam_subsingleton subsingleton_singleton
+
+@[to_additive (attr := simp)]
+theorem diam_one [One α] : diam (1 : Set α) = 0 :=
+  diam_singleton
+
+theorem diam_iUnion_mem_option {ι : Type*} (o : Option ι) (s : ι → Set α) :
+    diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i) := by cases o <;> simp
+
+theorem diam_insert : diam (insert x s) = max (⨆ y ∈ s, edist x y) (diam s) :=
+  eq_of_forall_ge_iff fun d => by
+    simp only [diam_le_iff, forall_mem_insert, edist_self, edist_comm x, max_le_iff, iSup_le_iff,
+      zero_le, true_and_iff, forall_and, and_self_iff, ← and_assoc]
+
+theorem diam_pair : diam ({x, y} : Set α) = edist x y := by
+  simp only [iSup_singleton, diam_insert, diam_singleton, ENNReal.max_zero_right]
+
+theorem diam_triple : diam ({x, y, z} : Set α) = max (max (edist x y) (edist x z)) (edist y z) := by
+  simp only [diam_insert, iSup_insert, iSup_singleton, diam_singleton, ENNReal.max_zero_right,
+    ENNReal.sup_eq_max]
+
+/-- The diameter is monotonous with respect to inclusion -/
+@[gcongr]
+theorem diam_mono {s t : Set α} (h : s ⊆ t) : diam s ≤ diam t :=
+  diam_le fun _x hx _y hy => edist_le_diam_of_mem (h hx) (h hy)
+
+/-- The diameter of a union is controlled by the diameter of the sets, and the edistance
+between two points in the sets. -/
+theorem diam_union {t : Set α} (xs : x ∈ s) (yt : y ∈ t) :
+    diam (s ∪ t) ≤ diam s + edist x y + diam t := by
+  have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t := fun a ha b hb =>
+    calc
+      edist a b ≤ edist a x + edist x y + edist y b := edist_triangle4 _ _ _ _
+      _ ≤ diam s + edist x y + diam t :=
+        add_le_add (add_le_add (edist_le_diam_of_mem ha xs) le_rfl) (edist_le_diam_of_mem yt hb)
+  refine diam_le fun a ha b hb => ?_
+  cases' (mem_union _ _ _).1 ha with h'a h'a <;> cases' (mem_union _ _ _).1 hb with h'b h'b
+  · calc
+      edist a b ≤ diam s := edist_le_diam_of_mem h'a h'b
+      _ ≤ diam s + (edist x y + diam t) := le_self_add
+      _ = diam s + edist x y + diam t := (add_assoc _ _ _).symm
+  · exact A a h'a b h'b
+  · have Z := A b h'b a h'a
+    rwa [edist_comm] at Z
+  · calc
+      edist a b ≤ diam t := edist_le_diam_of_mem h'a h'b
+      _ ≤ diam s + edist x y + diam t := le_add_self
+
+theorem diam_union' {t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t := by
+  let ⟨x, ⟨xs, xt⟩⟩ := h
+  simpa using diam_union xs xt
+
+theorem diam_closedBall {r : ℝ≥0∞} : diam (closedBall x r) ≤ 2 * r :=
+  diam_le fun a ha b hb =>
+    calc
+      edist a b ≤ edist a x + edist b x := edist_triangle_right _ _ _
+      _ ≤ r + r := add_le_add ha hb
+      _ = 2 * r := (two_mul r).symm
+
+theorem diam_ball {r : ℝ≥0∞} : diam (ball x r) ≤ 2 * r :=
+  le_trans (diam_mono ball_subset_closedBall) diam_closedBall
+
+theorem diam_pi_le_of_le {π : β → Type*} [Fintype β] [∀ b, PseudoEMetricSpace (π b)]
+    {s : ∀ b : β, Set (π b)} {c : ℝ≥0∞} (h : ∀ b, diam (s b) ≤ c) : diam (Set.pi univ s) ≤ c := by
+  refine diam_le fun x hx y hy => edist_pi_le_iff.mpr ?_
+  rw [mem_univ_pi] at hx hy
+  exact fun b => diam_le_iff.1 (h b) (x b) (hx b) (y b) (hy b)
+
+end
+
+section
+variable [EMetricSpace β] {s : Set β}
+
+theorem diam_eq_zero_iff : diam s = 0 ↔ s.Subsingleton :=
+  ⟨fun h _x hx _y hy => edist_le_zero.1 <| h ▸ edist_le_diam_of_mem hx hy, diam_subsingleton⟩
+
+theorem diam_pos_iff : 0 < diam s ↔ s.Nontrivial := by
+  simp only [pos_iff_ne_zero, Ne, diam_eq_zero_iff, Set.not_subsingleton_iff]
+
+theorem diam_pos_iff' : 0 < diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y := by
+  simp only [diam_pos_iff, Set.Nontrivial, exists_prop]
+
+end
+
+end EMetric

Mathlib/Topology/EMetricSpace/Lipschitz.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rohan Mitta, Kevin Buzzard, Alistair Tucker, Johannes Hölzl, Yury Kudryashov
 -/
 import Mathlib.Logic.Function.Iterate
-import Mathlib.Topology.EMetricSpace.Basic
+import Mathlib.Topology.EMetricSpace.Diam
 import Mathlib.Tactic.GCongr
 
 /-!

Mathlib/Topology/EMetricSpace/Paracompact.lean

@@ -5,8 +5,8 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.SetTheory.Ordinal.Basic
 import Mathlib.Tactic.GCongr
-import Mathlib.Topology.EMetricSpace.Basic
 import Mathlib.Topology.Compactness.Paracompact
+import Mathlib.Topology.EMetricSpace.Basic
 
 /-!
 # (Extended) metric spaces are paracompact

Mathlib/Topology/Instances/Discrete.lean

@@ -5,7 +5,6 @@ Authors: Rémy Degenne
 -/
 import Mathlib.Order.SuccPred.Basic
 import Mathlib.Topology.Order.Basic
-import Mathlib.Topology.Metrizable.Uniformity
 
 /-!
 # Instances related to the discrete topology
@@ -110,8 +109,3 @@ theorem discreteTopology_iff_orderTopology_of_pred_succ [LinearOrder α] [PredOr
 instance (priority := 100) DiscreteTopology.orderTopology_of_pred_succ [h : DiscreteTopology α]
     [LinearOrder α] [PredOrder α] [SuccOrder α] : OrderTopology α :=
   discreteTopology_iff_orderTopology_of_pred_succ.mp h
-
-instance (priority := 100) DiscreteTopology.metrizableSpace [DiscreteTopology α] :
-    MetrizableSpace α := by
-  obtain rfl := DiscreteTopology.eq_bot (α := α)
-  exact @UniformSpace.metrizableSpace α ⊥ (isCountablyGenerated_principal _) _

Mathlib/Topology/Instances/ENNReal.lean

@@ -9,6 +9,8 @@ import Mathlib.Topology.Instances.NNReal
 import Mathlib.Topology.EMetricSpace.Lipschitz
 import Mathlib.Topology.Metrizable.Basic
 import Mathlib.Topology.Order.T5
+import Mathlib.Topology.MetricSpace.Pseudo.Real
+import Mathlib.Topology.Metrizable.Uniformity
 
 /-!
 # Topology on extended non-negative reals

Mathlib/Topology/Instances/Int.lean

@@ -8,8 +8,8 @@ import Mathlib.Data.Int.SuccPred
 import Mathlib.Data.Int.ConditionallyCompleteOrder
 import Mathlib.Topology.Instances.Discrete
 import Mathlib.Topology.MetricSpace.Bounded
-import Mathlib.Topology.MetricSpace.Pseudo.Lemmas
 import Mathlib.Order.Filter.Archimedean
+import Mathlib.Topology.MetricSpace.Basic
 
 /-!
 # Topology on the integers

Mathlib/Topology/Instances/Nat.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Topology.Instances.Int
+import Mathlib.Data.Nat.Lattice
 
 /-!
 # Topology on the natural numbers

Mathlib/Topology/Instances/RatLemmas.lean

@@ -6,6 +6,7 @@ Authors: Yury Kudryashov
 import Mathlib.Topology.Instances.Irrational
 import Mathlib.Topology.Instances.Rat
 import Mathlib.Topology.Compactification.OnePoint
+import Mathlib.Topology.Metrizable.Uniformity
 
 /-!
 # Additional lemmas about the topology on rational numbers

Mathlib/Topology/Instances/Real.lean

@@ -12,6 +12,7 @@ import Mathlib.Topology.Algebra.UniformMulAction
 import Mathlib.Topology.Algebra.Star
 import Mathlib.Topology.Instances.Int
 import Mathlib.Topology.Order.Bornology
+import Mathlib.Topology.Metrizable.Basic
 
 /-!
 # Topological properties of ℝ