tendsto_norm_div_self_nhdsNE — Mathlib

English

For a fixed a ≠ 0 in a normed group E, the map x ↦ ∥x/a∥ tends to 0 as x→a, x ≠ a.

Русский

Для фиксированного a ≠ 0 в нормированной группе E отображение x ↦ ∥x/a∥ стремится к 0 при x→a, x≠a.

LaTeX

$$$\\lim_{x\\to a, x\\neq a} \\|x/a\\| = 0$.$$

Lean4

@[to_additive]
theorem tendsto_norm_div_self_nhdsNE (a : E) : Tendsto (fun x => ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0) :=
  (tendsto_norm_div_self a).inf <| tendsto_principal_principal.2 fun _x hx => norm_pos_iff'.2 <| div_ne_one.2 hx

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