tendsto_norm_zpow_nhdsNE_zero_atTop

English

If m < 0, the norm of x^m tends to infinity as x → 0, x ≠ 0.

Русский

Пусть m < 0; тогда норма x^m стремится к бесконечности при x → 0, x ≠ 0.

LaTeX

$$$\text{If } m \in \mathbb{Z}, m < 0, \; \mathrm{Tendsto}(\lambda x. \|x^{m}\|) (\mathcal{N}_{\neq} 0) \; \text{to } \text{atTop}.$$$

Lean4

theorem tendsto_norm_zpow_nhdsNE_zero_atTop {m : ℤ} (hm : m < 0) : Tendsto (fun x : α ↦ ‖x ^ m‖) (𝓝[≠] 0) atTop :=
  by
  obtain ⟨m, rfl⟩ := neg_surjective m
  rw [neg_lt_zero] at hm
  lift m to ℕ using hm.le
  rw [Int.natCast_pos] at hm
  simp only [norm_pow, zpow_neg, zpow_natCast, ← inv_pow]
  exact (tendsto_pow_atTop hm.ne').comp NormedField.tendsto_norm_inv_nhdsNE_zero_atTop

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