From ea44d8643bb65cb7c722f4108a959d913f1421d7 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 26 Dec 2024 12:51:48 -0600
Subject: [PATCH] feat(MetricSpace): add `Metric.biInter_gt_ball` etc

---
 Mathlib/Order/Basic.lean                       |  7 +++++++
 .../Topology/MetricSpace/Pseudo/Lemmas.lean    | 18 ++++++++++++++++++
 2 files changed, 25 insertions(+)

diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
index a76d787182917..7649faffca083 100644
--- a/Mathlib/Order/Basic.lean
+++ b/Mathlib/Order/Basic.lean
@@ -1281,6 +1281,13 @@ theorem eq_of_le_of_forall_ge_of_dense [LinearOrder α] [DenselyOrdered α] {a
     (h₂ : ∀ a₃ < a₁, a₃ ≤ a₂) : a₁ = a₂ :=
   (le_of_forall_ge_of_dense h₂).antisymm h₁
 
+theorem forall_lt_le_iff [LinearOrder α] [DenselyOrdered α] {a b : α} : (∀ c < a, c ≤ b) ↔ a ≤ b :=
+  ⟨le_of_forall_ge_of_dense, fun hab _c hca ↦ hca.le.trans hab⟩
+
+theorem forall_gt_ge_iff [LinearOrder α] [DenselyOrdered α] {a b : α} :
+    (∀ c, a < c → b ≤ c) ↔ b ≤ a :=
+  forall_lt_le_iff (α := αᵒᵈ)
+
 theorem dense_or_discrete [LinearOrder α] (a₁ a₂ : α) :
     (∃ a, a₁ < a ∧ a < a₂) ∨ (∀ a, a₁ < a → a₂ ≤ a) ∧ ∀ a < a₂, a ≤ a₁ :=
   or_iff_not_imp_left.2 fun h ↦
diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean b/Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
index 2a58189df2473..6b6cd86da53a2 100644
--- a/Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
+++ b/Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
@@ -89,4 +89,22 @@ lemma exists_isCompact_closedBall [WeaklyLocallyCompactSpace α] (x : α) :
     eventually_nhdsWithin_of_eventually_nhds (eventually_isCompact_closedBall x)
   simpa only [and_comm] using (this.and self_mem_nhdsWithin).exists
 
+theorem biInter_gt_closedBall (x : α) (r : ℝ) : ⋂ r' > r, closedBall x r' = closedBall x r := by
+  ext
+  simp [forall_gt_ge_iff]
+
+theorem biInter_gt_ball (x : α) (r : ℝ) : ⋂ r' > r, ball x r' = closedBall x r := by
+  ext
+  simp [forall_lt_iff_le']
+
+theorem biUnion_lt_ball (x : α) (r : ℝ) : ⋃ r' < r, ball x r' = ball x r := by
+  ext
+  rw [← not_iff_not]
+  simp [forall_lt_le_iff]
+
+theorem biUnion_lt_closedBall (x : α) (r : ℝ) : ⋃ r' < r, closedBall x r' = ball x r := by
+  ext
+  rw [← not_iff_not]
+  simp [forall_lt_iff_le]
+
 end Metric