English
In a pseudometric space, a family F: β → γ → α is uniformly Cauchy on a set s if and only if for every ε>0 there exists N such that for all m≥N, n≥N and x∈s, dist(F(m,x), F(n,x))<ε.
Русский
В псевдометрическом пространстве семейство F: β → γ → α является равномерно Коши на множестве s тогда и только тогда, когда для каждого ε>0 существует N, такой что для всех m≥N, n≥N и x∈s выполняется dist(F(m,x), F(n,x))<ε.
LaTeX
$$$\\displaystyle \\text{UniformCauchySeqOn}(F, atTop, s) \\iff \\forall \\varepsilon>0,\\; \\exists N, \\forall m\\ge N, \\forall n\\ge N, \\forall x\\in s,\\; \\operatorname{dist}(F(m,x),F(n,x))<\\varepsilon.$$$
Lean4
/-- In a pseudometric space, uniform Cauchy sequences are characterized by the fact that,
eventually, the distance between all its elements is uniformly, arbitrarily small. -/
theorem uniformCauchySeqOn_iff {γ : Type*} {F : β → γ → α} {s : Set γ} :
UniformCauchySeqOn F atTop s ↔ ∀ ε > (0 : ℝ), ∃ N : β, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε :=
by
constructor
· intro h ε hε
let u := {a : α × α | dist a.fst a.snd < ε}
have hu : u ∈ 𝓤 α := Metric.mem_uniformity_dist.mpr ⟨ε, hε, by simp [u]⟩
rw [← Filter.eventually_atTop_prod_self' (p := fun m => ∀ x ∈ s, dist (F m.fst x) (F m.snd x) < ε)]
specialize h u hu
rw [prod_atTop_atTop_eq] at h
exact h.mono fun n h x hx => h x hx
· intro h u hu
rcases Metric.mem_uniformity_dist.mp hu with ⟨ε, hε, hab⟩
rcases h ε hε with ⟨N, hN⟩
rw [prod_atTop_atTop_eq, eventually_atTop]
use (N, N)
intro b hb x hx
rcases hb with ⟨hbl, hbr⟩
exact hab (hN b.fst hbl.ge b.snd hbr.ge x hx)
