Theorems · Theorem · functional analysis

WithSeminorms.congr

∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} {ι' : Type u_10} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 E ι'} [t : TopologicalSpace E],
  WithSeminorms p → Seminorm.IsBounded p q LinearMap.id → Seminorm.IsBounded q p LinearMap.id → WithSeminorms q

Two families of seminorms p and q on the same space generate the same topology if each p i is bounded by some C • Finset.sup s q and vice-versa. We formulate these boundedness assumptions as Seminorm.IsBounded q p LinearMap.id (and vice-versa) to reuse the API. Furthermore, we don't actually state it as an equality of topologies but as a way to deduce WithSeminorms q from WithSeminorms p, since this should be more useful in practice.

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedFieldAddCommGroupModuleTopologicalSpace