English
As a corollary to the previous result, if deg p > 0 and leadingCoeff nonzero, then for any abv and z with abv ∘ z → atTop, we have abv(p.eval z) → atTop.
Русский
Следствие из предыдущего: если deg p > 0 и p.leadingCoeff ≠ 0, то при abv ∘ z → atTop имеем abv(p.eval(z)) → atTop.
LaTeX
$$$\\forall p\\, (hd: 0 < \\deg p)\\, (hf: p.leadingCoeff \\neq 0),\\; \\forall l \\; \\forall z:\\; Tendsto (abv \\circ z) l \\text{ atTop} \\Rightarrow\\; Tendsto (abv (p.eval (z x))) l \\text{ atTop}$$$
Lean4
theorem tendsto_abv_atTop {R k α : Type*} [Ring R] [Field k] [LinearOrder k] [IsStrictOrderedRing k] (abv : R → k)
[IsAbsoluteValue abv] (p : R[X]) (h : 0 < degree p) {l : Filter α} {z : α → R} (hz : Tendsto (abv ∘ z) l atTop) :
Tendsto (fun x => abv (p.eval (z x))) l atTop :=
by
apply tendsto_abv_eval₂_atTop _ _ _ h _ hz
exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)
