Theorems · Theorem · functional analysis

Seminorm.map_eq_zero_of_norm_eq_zero

∀ {𝕜 : Type u_2} {F : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (q : Seminorm 𝕜 F), Continuous ⇑q → ∀ {x : F}, ‖x‖ = 0 → q x = 0

In a semi-NormedSpace, a continuous seminorm is zero on elements of norm 0.

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

1 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpace