tendsto_normSq_cocompact_atTop — Mathlib

English

The function z ↦ |z|^2 is proper: it tends to infinity along the cocompact filter on ℂ.

Русский

Функция z ↦ |z|^2 является proper: вдоль фильтра cocompact ℂ значения стремятся к бесконечности.

LaTeX

$$$$ \\operatorname{Tendsto}(\\operatorname{normSq})\\bigl(\\operatorname{cocompact}(\\mathbb{C})\\bigr)\\operatorname{atTop}. $$$$

Lean4

/-- The `normSq` function on `ℂ` is proper. -/
theorem tendsto_normSq_cocompact_atTop : Tendsto normSq (cocompact ℂ) atTop := by
  simpa [norm_mul_self_eq_normSq] using
    tendsto_norm_cocompact_atTop.atTop_mul_atTop₀ (tendsto_norm_cocompact_atTop (E := ℂ))

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