From 83e44ebff54f7dbc819bb958ee9572b0d89ce296 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 1 Nov 2023 11:01:23 +0000
Subject: [PATCH] chore: forward-port leanprover-community/mathlib#19028

This was "feat(topology/metric_space): diameter of pointwise zero and addition"
---
 Mathlib/Analysis/Normed/Group/Pointwise.lean  | 19 ++++++++++++-
 Mathlib/Topology/Bornology/Basic.lean         |  6 +++++
 Mathlib/Topology/EMetricSpace/Basic.lean      | 12 +++++++--
 .../Topology/MetricSpace/Antilipschitz.lean   | 24 +++++++++++++++--
 Mathlib/Topology/MetricSpace/Basic.lean       |  2 +-
 Mathlib/Topology/MetricSpace/Bounded.lean     |  8 +++++-
 Mathlib/Topology/MetricSpace/Lipschitz.lean   | 27 ++++++++++++++++++-
 7 files changed, 90 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Group/Pointwise.lean b/Mathlib/Analysis/Normed/Group/Pointwise.lean
index 3baef382f1d72b..7e5cc107193209 100644
--- a/Mathlib/Analysis/Normed/Group/Pointwise.lean
+++ b/Mathlib/Analysis/Normed/Group/Pointwise.lean
@@ -5,8 +5,9 @@ Authors: Sébastien Gouëzel, Yaël Dillies
 -/
 import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.Topology.MetricSpace.HausdorffDistance
+import Topology.MetricSpace.IsometricSmul
 
-#align_import analysis.normed.group.pointwise from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
+#align_import analysis.normed.group.pointwise from "leanprover-community/mathlib"@"c8f305514e0d47dfaa710f5a52f0d21b588e6328"
 
 /-!
 # Properties of pointwise addition of sets in normed groups
@@ -24,6 +25,7 @@ section SeminormedGroup
 
 variable [SeminormedGroup E] {ε δ : ℝ} {s t : Set E} {x y : E}
 
+-- note: we can't use `LipschitzOnWith.isBounded_image2` here without adding `[IsometricSMul E E]`
 @[to_additive]
 theorem Bornology.IsBounded.mul (hs : IsBounded s) (ht : IsBounded t) : IsBounded (s * t) := by
   obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le'
@@ -34,6 +36,12 @@ theorem Bornology.IsBounded.mul (hs : IsBounded s) (ht : IsBounded t) : IsBounde
 #align metric.bounded.mul Bornology.IsBounded.mul
 #align metric.bounded.add Bornology.IsBounded.add
 
+@[to_additive]
+theorem Bornology.IsBounded.of_mul (hst : Bounded (s * t)) : Bounded s ∨ Bounded t :=
+  AntilipschitzWith.isBounded_of_image2_left _ (fun x => (isometry_mul_right x).antilipschitz) hst
+#align metric.bounded.of_mul Bornology.IsBounded.of_mul
+#align metric.bounded.of_add Bornology.IsBounded.of_add
+
 @[to_additive]
 theorem Bornology.IsBounded.inv : IsBounded s → IsBounded s⁻¹ := by
   simp_rw [isBounded_iff_forall_norm_le', ← image_inv, ball_image_iff, norm_inv']
@@ -69,6 +77,15 @@ theorem infEdist_inv (x : E) (s : Set E) : infEdist x⁻¹ s = infEdist x s⁻¹
 #align inf_edist_inv infEdist_inv
 #align inf_edist_neg infEdist_neg
 
+@[to_additive]
+theorem ediam_mul_le (x y : Set E) : EMetric.diam (x * y) ≤ EMetric.diam x + EMetric.diam y :=
+  (LipschitzOnWith.ediam_image2_le (· * ·) _ _
+        (fun _ _ => (isometry_mul_right _).lipschitz.LipschitzOnWith _) fun _ _ =>
+        (isometry_mul_left _).lipschitz.LipschitzOnWith _).trans_eq <|
+    by simp only [ENNReal.coe_one, one_mul]
+#align ediam_mul_le ediam_mul_le
+#align ediam_add_le ediam_add_le
+
 end EMetric
 
 variable (ε δ s t x y)
diff --git a/Mathlib/Topology/Bornology/Basic.lean b/Mathlib/Topology/Bornology/Basic.lean
index fc3438f419ed3f..34b1b3c40a9af1 100644
--- a/Mathlib/Topology/Bornology/Basic.lean
+++ b/Mathlib/Topology/Bornology/Basic.lean
@@ -173,6 +173,12 @@ theorem isBounded_empty : IsBounded (∅ : Set α) := by
   exact univ_mem
 #align bornology.is_bounded_empty Bornology.isBounded_empty
 
+theorem nonempty_of_not_isBounded (h : ¬IsBounded s) : s.Nonempty := by
+  rw [nonempty_iff_ne_empty]
+  rintro rfl
+  exact h isBounded_empty
+#align metric.nonempty_of_unbounded Bornology.nonempty_of_not_isBounded
+
 @[simp]
 theorem isBounded_singleton : IsBounded ({x} : Set α) := by
   rw [isBounded_def]
diff --git a/Mathlib/Topology/EMetricSpace/Basic.lean b/Mathlib/Topology/EMetricSpace/Basic.lean
index 83dd6fa5973267..e61e05c1d11420 100644
--- a/Mathlib/Topology/EMetricSpace/Basic.lean
+++ b/Mathlib/Topology/EMetricSpace/Basic.lean
@@ -8,7 +8,7 @@ import Mathlib.Topology.UniformSpace.Pi
 import Mathlib.Topology.UniformSpace.UniformConvergence
 import Mathlib.Topology.UniformSpace.UniformEmbedding
 
-#align_import topology.metric_space.emetric_space from "leanprover-community/mathlib"@"195fcd60ff2bfe392543bceb0ec2adcdb472db4c"
+#align_import topology.metric_space.emetric_space from "leanprover-community/mathlib"@"c8f305514e0d47dfaa710f5a52f0d21b588e6328"
 
 /-!
 # Extended metric spaces
@@ -29,7 +29,9 @@ to `EMetricSpace` at the end.
 -/
 
 
-open Set Filter Classical Uniformity Topology BigOperators NNReal ENNReal
+open Set Filter Classical
+
+open scoped Uniformity Topology BigOperators Filter NNReal ENNReal Pointwise
 
 universe u v w
 
@@ -925,6 +927,12 @@ theorem diam_singleton : diam ({x} : Set α) = 0 :=
   diam_subsingleton subsingleton_singleton
 #align emetric.diam_singleton EMetric.diam_singleton
 
+@[to_additive (attr := simp)]
+theorem diam_one [One α] : diam (1 : Set α) = 0 :=
+  diam_singleton
+#align emetric.diam_one EMetric.diam_one
+#align emetric.diam_zero EMetric.diam_zero
+
 theorem diam_iUnion_mem_option {ι : Type*} (o : Option ι) (s : ι → Set α) :
     diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i) := by cases o <;> simp
 #align emetric.diam_Union_mem_option EMetric.diam_iUnion_mem_option
diff --git a/Mathlib/Topology/MetricSpace/Antilipschitz.lean b/Mathlib/Topology/MetricSpace/Antilipschitz.lean
index 95e859d0c914ab..c8acafc12eb0ee 100644
--- a/Mathlib/Topology/MetricSpace/Antilipschitz.lean
+++ b/Mathlib/Topology/MetricSpace/Antilipschitz.lean
@@ -6,7 +6,7 @@ Authors: Yury Kudryashov
 import Mathlib.Topology.MetricSpace.Lipschitz
 import Mathlib.Topology.UniformSpace.CompleteSeparated
 
-#align_import topology.metric_space.antilipschitz from "leanprover-community/mathlib"@"97f079b7e89566de3a1143f887713667328c38ba"
+#align_import topology.metric_space.antilipschitz from "leanprover-community/mathlib"@"c8f305514e0d47dfaa710f5a52f0d21b588e6328"
 
 /-!
 # Antilipschitz functions
@@ -218,7 +218,8 @@ namespace AntilipschitzWith
 
 open Metric
 
-variable [PseudoMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0} {f : α → β}
+variable [PseudoMetricSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ]
+variable {K : ℝ≥0} {f : α → β}
 
 theorem isBounded_preimage (hf : AntilipschitzWith K f) {s : Set β} (hs : IsBounded s) :
     IsBounded (f ⁻¹' s) :=
@@ -243,6 +244,25 @@ protected theorem properSpace {α : Type*} [MetricSpace α] {K : ℝ≥0} {f : 
   exact (hf.image_preimage _).symm
 #align antilipschitz_with.proper_space AntilipschitzWith.properSpace
 
+theorem isBounded_of_image2_left (f : α → β → γ) {K₁ : ℝ≥0}
+    (hf : ∀ b, AntilipschitzWith K₁ fun a => f a b) {s : Set α} {t : Set β}
+    (hst : IsBounded (Set.image2 f s t)) : IsBounded s ∨ IsBounded t := by
+  contrapose! hst
+  obtain ⟨b, hb⟩ : t.Nonempty := nonempty_of_not_isBounded hst.2
+  have : ¬IsBounded (Set.image2 f s {b}) := by
+    intro h
+    apply hst.1
+    rw [Set.image2_singleton_right] at h
+    replace h := (hf b).isBounded_preimage h
+    refine' h.subset (subset_preimage_image _ _)
+  exact mt (IsBounded.subset · (image2_subset subset_rfl (singleton_subset_iff.mpr hb))) this
+#align antilipschitz_with.bounded_of_image2_left AntilipschitzWith.isBounded_of_image2_left
+
+theorem isBounded_of_image2_right {f : α → β → γ} {K₂ : ℝ≥0} (hf : ∀ a, AntilipschitzWith K₂ (f a))
+    {s : Set α} {t : Set β} (hst : IsBounded (Set.image2 f s t)) : IsBounded s ∨ IsBounded t :=
+  Or.symm <| isBounded_of_image2_left (flip f) hf <| image2_swap f s t ▸ hst
+#align antilipschitz_with.bounded_of_image2_right AntilipschitzWith.isBounded_of_image2_right
+
 end AntilipschitzWith
 
 theorem LipschitzWith.to_rightInverse [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0}
diff --git a/Mathlib/Topology/MetricSpace/Basic.lean b/Mathlib/Topology/MetricSpace/Basic.lean
index a96f659d87db90..e85dec3035d876 100644
--- a/Mathlib/Topology/MetricSpace/Basic.lean
+++ b/Mathlib/Topology/MetricSpace/Basic.lean
@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Robert Y. Lewis, Johannes Hölzl, Mario Carneiro, Sébas
 -/
 import Mathlib.Topology.MetricSpace.PseudoMetric
 
-#align_import topology.metric_space.basic from "leanprover-community/mathlib"@"8047de4d911cdef39c2d646165eea972f7f9f539"
+#align_import topology.metric_space.basic from "leanprover-community/mathlib"@"c8f305514e0d47dfaa710f5a52f0d21b588e6328"
 
 /-!
 # Metric spaces
diff --git a/Mathlib/Topology/MetricSpace/Bounded.lean b/Mathlib/Topology/MetricSpace/Bounded.lean
index d967e908e7cafe..281f94be3db5e8 100644
--- a/Mathlib/Topology/MetricSpace/Bounded.lean
+++ b/Mathlib/Topology/MetricSpace/Bounded.lean
@@ -29,7 +29,7 @@ metric, pseudo_metric, bounded, diameter, Heine-Borel theorem
 -/
 
 open Set Filter  Bornology
-open scoped ENNReal Uniformity Topology
+open scoped ENNReal Uniformity Topology Pointwise
 
 universe u v w
 
@@ -363,6 +363,12 @@ theorem diam_singleton : diam ({x} : Set α) = 0 :=
   diam_subsingleton subsingleton_singleton
 #align metric.diam_singleton Metric.diam_singleton
 
+@[to_additive (attr := simp)]
+theorem diam_one [One α] : diam (1 : Set α) = 0 :=
+  diam_singleton
+#align metric.diam_one Metric.diam_one
+#align metric.diam_zero Metric.diam_zero
+
 -- Does not work as a simp-lemma, since {x, y} reduces to (insert y {x})
 theorem diam_pair : diam ({x, y} : Set α) = dist x y := by
   simp only [diam, EMetric.diam_pair, dist_edist]
diff --git a/Mathlib/Topology/MetricSpace/Lipschitz.lean b/Mathlib/Topology/MetricSpace/Lipschitz.lean
index c81b6bc3bafa65..7d3808063b35d6 100644
--- a/Mathlib/Topology/MetricSpace/Lipschitz.lean
+++ b/Mathlib/Topology/MetricSpace/Lipschitz.lean
@@ -9,7 +9,7 @@ import Mathlib.Topology.Bornology.Hom
 import Mathlib.Topology.MetricSpace.Basic
 import Mathlib.Topology.MetricSpace.Bounded
 
-#align_import topology.metric_space.lipschitz from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
+#align_import topology.metric_space.lipschitz from "leanprover-community/mathlib"@"c8f305514e0d47dfaa710f5a52f0d21b588e6328"
 
 /-!
 # Lipschitz continuous functions
@@ -541,6 +541,19 @@ protected theorem prod {g : α → γ} {Kf Kg : ℝ≥0} (hf : LipschitzOnWith K
   rw [ENNReal.coe_mono.map_max, Prod.edist_eq, ENNReal.max_mul]
   exact max_le_max (hf hx hy) (hg hx hy)
 
+theorem ediam_image2_le (f : α → β → γ) {K₁ K₂ : ℝ≥0} (s : Set α) (t : Set β)
+    (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun a => f a b) s)
+    (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) :
+    EMetric.diam (Set.image2 f s t) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t := by
+  apply EMetric.diam_le
+  rintro _ ⟨a₁, b₁, ha₁, hb₁, rfl⟩ _ ⟨a₂, b₂, ha₂, hb₂, rfl⟩
+  refine' (edist_triangle _ (f a₂ b₁) _).trans _
+  exact
+    add_le_add
+      ((hf₁ b₁ hb₁ ha₁ ha₂).trans <| ENNReal.mul_left_mono <| EMetric.edist_le_diam_of_mem ha₁ ha₂)
+      ((hf₂ a₂ ha₂ hb₁ hb₂).trans <| ENNReal.mul_left_mono <| EMetric.edist_le_diam_of_mem hb₁ hb₂)
+#align lipschitz_on_with.ediam_image2_le LipschitzOnWith.ediam_image2_le
+
 end EMetric
 
 section Metric
@@ -592,6 +605,18 @@ protected theorem iff_le_add_mul {f : α → ℝ} {K : ℝ≥0} :
   ⟨LipschitzOnWith.le_add_mul, LipschitzOnWith.of_le_add_mul K⟩
 #align lipschitz_on_with.iff_le_add_mul LipschitzOnWith.iff_le_add_mul
 
+theorem isBounded_image2 (f : α → β → γ) {K₁ K₂ : ℝ≥0} {s : Set α} {t : Set β}
+    (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t)
+    (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun a => f a b) s)
+    (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) : Bornology.IsBounded (Set.image2 f s t) :=
+  Metric.isBounded_iff_ediam_ne_top.2 <|
+    ne_top_of_le_ne_top
+      (ENNReal.add_ne_top.mpr
+        ⟨ENNReal.mul_ne_top ENNReal.coe_ne_top hs.ediam_ne_top,
+          ENNReal.mul_ne_top ENNReal.coe_ne_top ht.ediam_ne_top⟩)
+      (ediam_image2_le _ _ _ hf₁ hf₂)
+#align lipschitz_on_with.bounded_image2 LipschitzOnWith.isBounded_image2
+
 end Metric
 
 end LipschitzOnWith