tendsto_const_mul_pow_nhds_iff

Mathlib.Topology.Algebra.Order.Field

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

← MathLib Explorer

English

If f(x) → 0 from the left, then f(x)^{-1} → −∞.

Русский

Если f(x) → 0 слева, то 1/f(x) → −∞.

LaTeX

$$If f \xrightarrow{l} 0^- then f^{-1} \xrightarrow{l} -\infty.$$

Lean4

theorem tendsto_const_mul_pow_nhds_iff {n : ℕ} {c d : 𝕜} (hc : c ≠ 0) :
    Tendsto (fun x : 𝕜 => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d := by simp [tendsto_const_mul_pow_nhds_iff', hc]

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

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

Разделы

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

Аффилиация

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