feat(Topology/MetricSpace): metric ε-δ form of Heine–Cantor for ContinuousOn on a compact set

Add `ContinuousOn.exists_forall_dist_lt_of_isCompact` and its non-strict
variant `ContinuousOn.exists_forall_dist_le_of_isCompact`, unpacking
`IsCompact.uniformContinuousOn_of_continuous` through the metric ε-δ
characterizations `Metric.uniformContinuousOn_iff(_le)`.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: teorth

Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Topology.MetricSpace.Pseudo.Constructions
 public import Mathlib.Topology.Order.DenselyOrdered
 public import Mathlib.Topology.UniformSpace.Compact
+public import Mathlib.Topology.UniformSpace.HeineCantor
 
 /-!
 # Extra lemmas about pseudo-metric spaces
@@ -125,3 +126,17 @@ theorem lebesgue_number_lemma_of_metric {s : Set α} {ι : Sort*} {c : ι → Se
 theorem lebesgue_number_lemma_of_metric_sUnion {s : Set α} {c : Set (Set α)} (hs : IsCompact s)
     (hc₁ : ∀ t ∈ c, IsOpen t) (hc₂ : s ⊆ ⋃₀ c) : ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t := by
   rw [sUnion_eq_iUnion] at hc₂; simpa using lebesgue_number_lemma_of_metric hs (by simpa) hc₂
+
+/-- **Heine–Cantor** in metric ε-δ form: a function `f` continuous on a compact set `S` is
+uniformly continuous there, so for every `ε > 0` there is a `δ > 0` such that points of `S`
+within `δ` are mapped within `ε`. -/
+theorem ContinuousOn.exists_forall_dist_lt_of_isCompact {β : Type*} [PseudoMetricSpace β]
+    {S : Set α} (hS : IsCompact S) {f : α → β} (hf : ContinuousOn f S) {ε : ℝ} (hε : 0 < ε) :
+    ∃ δ > 0, ∀ x ∈ S, ∀ y ∈ S, dist x y < δ → dist (f x) (f y) < ε :=
+  Metric.uniformContinuousOn_iff.mp (hS.uniformContinuousOn_of_continuous hf) ε hε
+
+/-- Version of `ContinuousOn.exists_forall_dist_lt_of_isCompact` with non-strict inequalities. -/
+theorem ContinuousOn.exists_forall_dist_le_of_isCompact {β : Type*} [PseudoMetricSpace β]
+    {S : Set α} (hS : IsCompact S) {f : α → β} (hf : ContinuousOn f S) {ε : ℝ} (hε : 0 < ε) :
+    ∃ δ > 0, ∀ x ∈ S, ∀ y ∈ S, dist x y ≤ δ → dist (f x) (f y) ≤ ε :=
+  Metric.uniformContinuousOn_iff_le.mp (hS.uniformContinuousOn_of_continuous hf) ε hε