Theorems · Theorem · functional analysis

Seminorm.cont_withSeminorms_normedSpace

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

∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {ι : Type u_9} [inst : AddCommGroup E] [inst_1 : NormedField 𝕝]
  [inst_2 : Module 𝕝 E] [inst_3 : NormedField 𝕝₂] {τ₁₂ : 𝕝 →+* 𝕝₂} [inst_4 : RingHomIsometric τ₁₂] (F : Type u_11)
  [inst_5 : SeminormedAddCommGroup F] [inst_6 : NormedSpace 𝕝₂ F] [inst_7 : TopologicalSpace E] {p : ι → Seminorm 𝕝 E},
  WithSeminorms p → ∀ (f : E →ₛₗ[τ₁₂] F), (∃ s C, (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p) → Continuous ⇑f

Alias of WithSeminorms.continuous_normedSpace_rng.

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupNormedFieldModuleNormedFieldRingHomIsometricSeminormedAddCommGroupNormedSpaceTopologicalSpace