tendsto_norm_nhdsNE_one — Mathlib

English

The norm function on a normed group sends a punctured neighborhood of 1 to a neighborhood of 0, i.e., ∥x∥→0 as x→1 with x≠1.

Русский

Норма группы отображает любую окрестность вокруг 1 без 1 в окрестность 0: ∥x∥→0 при x→1, x≠1.

LaTeX

$$$\\operatorname{Tendsto}\\big(\\|\\cdot\\|: E\\to\\mathbb{R}\\big)\\,(nhdsWithin(1,\\mathbb{R}\\setminus\\{1\\}))\\,(nhdsWithin(0,\\mathbb{R}_{>0})).$$$

Lean4

/-- See `tendsto_norm_one` for a version with full neighborhoods. -/
@[to_additive /-- See `tendsto_norm_zero` for a version with full neighborhoods. -/
    ]
theorem tendsto_norm_nhdsNE_one : Tendsto (norm : E → ℝ) (𝓝[≠] 1) (𝓝[>] 0) :=
  tendsto_norm_one.inf <| tendsto_principal_principal.2 fun _ hx ↦ norm_pos_iff'.2 hx

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