English
Let f be a family f(n, z) taking values in a seminormed group G. The family f is uniformly Cauchy along l and l' if and only if the scaled quotients f(n.fst, z)/f(n.snd, z) converge uniformly to 1 on the product filter l × l'.
Русский
Пусть f: ι × κ → G принимает значения в семиномормированной группе G. Тогда условие равномерной сходимости задаётся эквивалентностью: семейство q(n, z) = f(n.fst, z)/f(n.snd, z) сходится равномерно к 1 на произведённом фильтре l × l'.
LaTeX
$$$\\text{UniformCauchySeqOnFilter}(f\\,l\\,l') \\;\\Longleftrightarrow\\; \\text{TendstoUniformlyOnFilter}\\big( (n,z) \\mapsto f(n.fst,z)/f(n.snd,z) \\big)\\, 1\\,(l\\times\\!l)l'.$$$
Lean4
@[to_additive]
theorem uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one {f : ι → κ → G} {l : Filter ι} {l' : Filter κ} :
UniformCauchySeqOnFilter f l l' ↔
TendstoUniformlyOnFilter (fun n : ι × ι => fun z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l' :=
by
refine ⟨fun hf u hu => ?_, fun hf u hu => ?_⟩
· obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu
refine
(hf {p : G × G | dist p.fst p.snd < ε} <| dist_mem_uniformity hε).mono fun x hx =>
H 1 (f x.fst.fst x.snd / f x.fst.snd x.snd) ?_
simpa [dist_eq_norm_div, norm_div_rev] using hx
· obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu
refine
(hf {p : G × G | dist p.fst p.snd < ε} <| dist_mem_uniformity hε).mono fun x hx =>
H (f x.fst.fst x.snd) (f x.fst.snd x.snd) ?_
simpa [dist_eq_norm_div, norm_div_rev] using hx
