English
If f and g are functions with values in ℂ such that f tends uniformly to g, then their real parts also tend uniformly: Re(f) → Re(g) uniformly.
Русский
Если функции f и g сходятся равномерно в ℂ, то их действительные части сходятся равномерно: Re(f) → Re(g) равномерно.
LaTeX
$$$\\operatorname{TendstoUniformly}(f,g,p) \\Rightarrow \\operatorname{TendstoUniformly}(\\lambda n x. \\operatorname{Re}(f(n,x)), \\lambda y. \\operatorname{Re}(g(y)), p)$$$
Lean4
protected theorem re {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ} {K : Set α} (hf : TendstoUniformlyOn f g p K) :
TendstoUniformlyOn (fun n x => (f n x).re) (fun y => (g y).re) p K := by
apply UniformContinuous.comp_tendstoUniformlyOn uniformlyContinuous_re hf
