Theorems · Theorem · functional analysis

Seminorm.bound_of_continuous

∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E],
  WithSeminorms p → ∀ (q : Seminorm 𝕜 E), Continuous ⇑q → ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Let E be a topological vector space (over a NontriviallyNormedField) whose topology is generated by some family of seminorms p, and let q be a seminorm on E. If q is continuous, then it is uniformly controlled by finitely many seminorms of p, that is there is some finset s of the index set and some C > 0 such that q ≤ C • s.sup p.

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpace