English
A sequence F: ι→α→β is uniformly Cauchy on a filter p with respect to p' if for every entourage U, the pairs (F i1 x, F i2 x) are eventually within U for i1,i2 from p and x from α with x in p'.
Русский
Последовательность F: ι→α→β равномерно Коши на фильтре p относительно p' если для каждого окружения U пары значений F i1 x, F i2 x в точности становятся ближе чем U для i1,i2 из p и x из α с x из p'.
LaTeX
$$$UniformCauchySeqOnFilter F\ p\ p' :\forall u\in 𝓤(β), \forallᶠ m : (ι×ι)×α \ in (p×ˢ p)×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u$$$
Lean4
/-- A sequence is uniformly Cauchy if eventually all of its pairwise differences are
uniformly bounded -/
def UniformCauchySeqOnFilter (F : ι → α → β) (p : Filter ι) (p' : Filter α) : Prop :=
∀ u ∈ 𝓤 β, ∀ᶠ m : (ι × ι) × α in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
