Theorems · Theorem · functional analysis

WithSeminorms.continuous_normedSpace_dom

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

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedFieldAddCommGroupNormedFieldModuleRingHomIsometricSeminormedAddCommGroupNormedSpaceTopologicalSpace