map_eq_zero_of_norm_zero — Mathlib

English

In a semi-normed space, a continuous seminorm vanishes on any element of norm zero; that is, if ||x|| = 0 then q(x) = 0.

Русский

В полугипрямом пространстве непрерывная семинормa обнуляется на любом элементе нулевой нормы; то есть если ||x|| = 0, то q(x) = 0.

LaTeX

$$$ q \\;\\text{is continuous} \\;\\Rightarrow\\; (\\|x\\| = 0) \\Rightarrow q(x) = 0 $$$

Lean4

/-- In a semi-`NormedSpace`, a continuous seminorm is zero on elements of norm `0`. -/
theorem map_eq_zero_of_norm_zero (q : Seminorm 𝕜 F) (hq : Continuous q) {x : F} (hx : ‖x‖ = 0) : q x = 0 :=
  (map_zero q) ▸ ((specializes_iff_mem_closure.mpr <| mem_closure_zero_iff_norm.mpr hx).map hq).eq.symm

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