tendsto_norm_inv_nhdsNE_zero_atTop

English

The inverse has controlled norm: Tendsto (‖x⁻¹‖) to infinity as x → 0.

Русский

Обратное имеет ограничение нормы: предел нормы обратного при подходе к нулю бесконечен.

LaTeX

$$$\mathrm{Tendsto}(\lambda x. \|x^{-1}\|) (\mathcal{N}_{\neq} 0) \; \text{to} \; \text{atTop}$$$

Lean4

theorem tendsto_norm_inv_nhdsNE_zero_atTop : Tendsto (fun x : α ↦ ‖x⁻¹‖) (𝓝[≠] 0) atTop :=
  (tendsto_inv_nhdsGT_zero.comp tendsto_norm_nhdsNE_zero).congr fun x ↦ (norm_inv x).symm

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