tendsto_norm_div_self — Mathlib

English

Let E be a seminormed group and x an element. As a approaches x, the norm of a divided by x tends to 0, i.e. a/x converges to the identity element in norm.

Русский

Пусть E — полусоединенная по норме группа, и возьмем элемент x. При приближении a к x, сущность ‖a/x‖ стремится к нулю, то есть a/x сходится к единице в норме.

LaTeX

$$$ \operatorname{Tendsto}\left( a \mapsto \|a/x\| \right)\left( \mathcal{N}(x) \right)\left( \mathcal{N}(0) \right). $$$

Lean4

@[to_additive]
theorem tendsto_norm_div_self (x : E) : Tendsto (fun a => ‖a / x‖) (𝓝 x) (𝓝 0) := by
  simpa [dist_eq_norm_div] using tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (x : E)) (𝓝 x) _)

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