English
Several dual statements express that multiplying by a fixed element on the left or on the right preserves or translates Tendsto toTop when the other factor tends to top (or is bounded). Variants exist for left/right and for ≤ or ≥ bounds.
Русский
Несколько двойственных утверждений выражают, что умножение на фиксированный элемент слева или справа сохраняет/перемещает предел к верхнему пределу, если другая часть стремится к верху (или ограничена). Существуют варианты для слева/справа и для ограничений ≤/≥.
LaTeX
$$$\\forall l:\\Filter\\ α,\\ \\forall f,g:\\alpha\\to G,\\Big(\\mathrm{Tendsto}\\ g\\ l\\ atTop\\Big)\\Rightarrow \\mathrm{Tendsto}(f\\cdot g)\\ l\\ atTop$$$
Lean4
@[to_additive]
theorem tendsto_atTop_mul_const_right (C : G) (hf : Tendsto f l atTop) : Tendsto (fun x => f x * C) l atTop :=
tendsto_atTop_mul_right_of_le' l C hf (univ_mem' fun _ => le_refl C)
