tendsto_norm_atTop_atTop

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#tendsto_norm_atTop_atTop

English

The function x ↦ ∥x∥ on the real line tends to infinity as x tends to infinity: Tendsto (‖x‖) atTop atTop.

Русский

Функция x ↦ ∥x∥ на множестве действительных чисел стремится к бесконечности при x → ∞: Tendsto (∥x∥) atTop atTop.

LaTeX

$$Tendsto (|x|) atTop atTop$$

Lean4

theorem tendsto_norm_atTop_atTop : Tendsto (norm : ℝ → ℝ) atTop atTop :=
  tendsto_abs_atTop_atTop

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru