English
Let p be a polynomial over a normed ring R, and suppose deg p > 0. If a net z in R satisfies ‖z‖ → ∞ along a filter l, then ‖p.eval(z)‖ → ∞ along l as well.
Русский
Пусть p — многочлен над нормированным кольцом R, deg p > 0. Если сетка z в R удовлетворяет ‖z‖ → ∞ по некоторому фильтру l, то и ‖p.eval(z)‖ → ∞ по l.
LaTeX
$$$0 < \\deg p \\;\\Rightarrow\\; \\forall l : \\text{Filter } \\alpha\\, \\forall z : \\alpha \\to R,\\; \\mathrm{Tendsto}(\\|z\\|)\\, l\\, \\mathrm{atTop} \\Rightarrow \\mathrm{Tendsto}(\\|p\\.eval(z)\\|)\\, l\\, \\mathrm{atTop}$$$
Lean4
theorem tendsto_norm_atTop (p : R[X]) (h : 0 < degree p) {l : Filter α} {z : α → R}
(hz : Tendsto (fun x => ‖z x‖) l atTop) : Tendsto (fun x => ‖p.eval (z x)‖) l atTop :=
p.tendsto_abv_atTop norm h hz
