tendsto_mul_left_cobounded — Mathlib

English

Multiplication by a nonzero a on the left tends to the cobounded filter.

Русский

Левое умножение на ненулевой a сходится к ковбоундированному фильтру.

LaTeX

$$$a \neq 0 \Rightarrow \mathrm{Tendsto}(x \mapsto a x) (\mathrm{cobounded}(\alpha)) (\mathrm{cobounded}(\alpha)).$$$

Lean4

/-- Multiplication on the left by a nonzero element of a normed division ring tends to infinity at
infinity. -/
theorem tendsto_mul_left_cobounded {a : α} (ha : a ≠ 0) : Tendsto (a * ·) (cobounded α) (cobounded α) :=
  (map_mul_left_cobounded ha).le

Похожие утверждения