Theorems · Theorem · functional analysis

Seminorm.bound_of_continuous_normedSpace

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

Let F be a semi-NormedSpace over a NontriviallyNormedField, and let q be a seminorm on F. If q is continuous, then it is uniformly controlled by the norm, that is there is some C > 0 such that ∀ x, q x ≤ C * ‖x‖. The continuity ensures boundedness on a ball of some radius ε. The nontriviality of the norm is then used to rescale any element into an element of norm in [ε/C, ε[, thus with a controlled image by q. The control of q at the original element follows by rescaling.

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpace