English
If TendstoUniformlyOn f g p K holds, then the imaginary parts converge uniformly on K: TendstoUniformlyOn (Im f) (Im g) p K.
Русский
Если выполняется равномерная сходимость по модулю Im, то Im(f) сходится равномерно: TendstoUniformlyOn (Im f) (Im g) p K.
LaTeX
$$$\\operatorname{TendstoUniformlyOn} f g p K \\Rightarrow \\operatorname{TendstoUniformlyOn}(\\lambda n x. \\operatorname{Im}(f(n,x)), \\lambda y. \\operatorname{Im}(g(y)), p, K)$$$
Lean4
protected theorem im {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ} {K : Set α} (hf : TendstoUniformlyOn f g p K) :
TendstoUniformlyOn (fun n x => (f n x).im) (fun y => (g y).im) p K := by
apply UniformContinuous.comp_tendstoUniformlyOn uniformlyContinuous_im hf
