Theorems · Theorem · functional analysis

WithSeminorms.continuous_iff_continuous_comp

∀ {𝕝 : Type u_4} {𝕝₂ : Type u_5} {E : Type u_6} {F : Type u_7} {ι' : 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 τ₁₂] {q : SeminormFamily 𝕝₂ F ι'}
  [inst_7 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_9 : TopologicalSpace F],
  WithSeminorms q → ∀ (f : E →ₛₗ[τ₁₂] F), Continuous ⇑f ↔ ∀ (i : ι'), Continuous ⇑((q i).comp f)

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommGroupNormedFieldModuleAddCommGroupNormedFieldModuleRingHomIsometricTopologicalSpaceIsTopologicalAddGroupTopologicalSpace