English
Let f: ι → κ → G be a family into a seminormed group G. Then Uniformly Cauchy on a set s is equivalent to TendstoUniformlyOn of the same scaled quotients to 1 on l ×ˢ l with target set s.
Русский
Пусть f: ι → κ → G, G — семиномед groups. Тогда условие равномерной сходимости на множестве s эквивалентно равномерной сходимости на произведении фильтров к 1 с тем же масштабированием.
LaTeX
$$$\\text{UniformCauchySeqOn}(f\\,l\\,s) \\;\\iff\\; \\text{TendstoUniformlyOn}\\big( (n,z)\\mapsto f(n.fst,z)/f(n.snd,z) \\big)\\,1\\,(l\\times\\!l)\\,s.$$$
Lean4
@[to_additive]
theorem uniformCauchySeqOn_iff_tendstoUniformlyOn_one {f : ι → κ → G} {s : Set κ} {l : Filter ι} :
UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n : ι × ι => fun z => f n.fst z / f n.snd z) 1 (l ×ˢ l) s := by
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, uniformCauchySeqOn_iff_uniformCauchySeqOnFilter,
SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one]
