feat(MetricSpace): add Metric.biInter_gt_ball etc (#20262)

Author: urkud

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 ↦

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