tendsto_zpow_atTop_atTop

Mathlib.Order.Filter.AtTopBot.Field

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

← MathLib Explorer

English

The map a ↦ a/k with k > 0 sends atTop to atTop.

Русский

Отображение a ↦ a/k при k > 0 переводит atTop в atTop.

LaTeX

$$$\operatorname{map}(a \mapsto a/k)\ atTop = atTop$$$

Lean4

theorem tendsto_zpow_atTop_atTop {n : ℤ} (hn : 0 < n) : Tendsto (fun x : α ↦ x ^ n) atTop atTop := by
  lift n to ℕ using hn.le; simp [(Int.natCast_pos.mp hn).ne']

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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