English
If a family of complex-valued functions f_n: X → ℂ converges uniformly to a function g: X → ℂ (with respect to a filter p on the index set), then the corresponding family of imaginary parts converges uniformly to the imaginary part of g. In symbols, if TendstoUniformly f g p, then TendstoUniformly (n ↦ (f n) Im) (g Im) p.
Русский
Если family из комплекснозначных функций f_n: X → ℂ сходится равномерно к функции g: X → ℂ по фильтру p на индексном множестве, то соответствующая последовательность мнимых частей сходится к мнимой части предела: TendstoUniformly f_im p, где f_im(n, x) = Im(f_n(x)) и g_im(x) = Im(g(x)).
LaTeX
$$$\displaystyle \text{If } f: \iota \to (\alpha \to \mathbb{C}),\ p \text{ a filter on } \iota,\ g: \alpha \to \mathbb{C}, \\ f \to g \text{ uniformly w.r.t. } p \Rightarrow (\lambda n x. \operatorname{Im}(f(n,x)) ) \to (\lambda y. \operatorname{Im}(g(y))) \text{ uniformly w.r.t. } p.$$$
Lean4
protected theorem im {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ} (hf : TendstoUniformly f g p) :
TendstoUniformly (fun n x => (f n x).im) (fun y => (g y).im) p := by
apply UniformContinuous.comp_tendstoUniformly uniformlyContinuous_im hf
