Theorems · Theorem · functional analysis

Seminorm.continuous_from_bounded

Deprecated since 2026-03-09Use WithSeminorms.continuous_of_isBounded instead.

∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι : Type u_9} {ι' : Type u_10} [inst : AddCommGroup E]
  [inst_1 : NormedField 𝕝] [inst_2 : Module 𝕝 E] [inst_3 : AddCommGroup F] [inst_4 : NormedField 𝕝₂]
  [inst_5 : Module 𝕝₂ F] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_6 : RingHomIsometric τ₁₂] {p : SeminormFamily 𝕝 E ι}
  {q : SeminormFamily 𝕝₂ F ι'} {x : TopologicalSpace E},
  WithSeminorms p →
    ∀ {x_1 : TopologicalSpace F}, WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), Seminorm.IsBounded p q f → Continuous ⇑f

Alias of WithSeminorms.continuous_of_isBounded.

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupNormedFieldModuleAddCommGroupNormedFieldModuleRingHomIsometric