mem_closure_one_iff_norm — Mathlib

English

An element x lies in the closure of {1} if and only if its norm is zero: x ∈ closure({1}) iff ‖x‖ = 0.

Русский

Элемент x принадлежит замыканию множества {1} тогда и только тогда, когда ‖x‖ = 0.

LaTeX

$$$ x \in \overline{\{1\}} \quad\Leftrightarrow\quad \|x\| = 0. $$$

Lean4

@[to_additive]
theorem mem_closure_one_iff_norm {x : E} : x ∈ closure ({ 1 } : Set E) ↔ ‖x‖ = 0 := by
  rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).ge_iff_eq']

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