tendsto_norm_div_self_nhdsGE — Mathlib

English

Let x ∈ E. The map a ↦ ‖a/x‖ tends to 0 when a tends to x, even with respect to the nhds within [0, ∞).

Русский

Пусть x ∈ E. Отображение a ↦ ‖a/x‖ стремится к 0, когда a стремится к x, даже в nhdsWithin 0 (Ici 0).

LaTeX

$$$ \operatorname{Tendsto}\left( a \mapsto \|a/x\| \right)\left( \nhds x \right)\left( \nhdsWithin 0 (\{ t \mid t \ge 0 \}) \right). $$$

Lean4

@[to_additive]
theorem tendsto_norm_div_self_nhdsGE (x : E) : Tendsto (fun a ↦ ‖a / x‖) (𝓝 x) (𝓝[≥] 0) :=
  tendsto_nhdsWithin_iff.mpr ⟨tendsto_norm_div_self x, by simp⟩

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