tendsto_mul_self_atTop

Mathlib.Order.Filter.AtTopBot.Ring

URI: https://scilib.ai/kg/mathlib#Filter.tendsto_mul_self_atTop

English

In a ordered ring, the map x ↦ x^2 tends to +∞ as x tends to +∞.

Русский

В упорядоченном кольце отображение x ↦ x^2 стремится к +∞ при x → +∞.

LaTeX

$$$ \operatorname{Tendsto}(\lambda x:\alpha, x^2)\ \mathrm{atTop}\ \mathrm{atTop}$$$

Lean4

theorem tendsto_mul_self_atTop : Tendsto (fun x : α => x * x) atTop atTop :=
  tendsto_id.atTop_mul_atTop₀ tendsto_id

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

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

Разделы

Аффилиация

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