𝕜 : Type ?u.658783
𝕜₂ : Type ?u.658786
𝕝 : Type u_2
𝕝₂ : Type u_4
E✝ : Type ?u.658795
F : Type u_3
G : Type ?u.658801
ι : Type u_5
ι' : Type ?u.658807
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E✝
inst✝¹⁵ : Module 𝕜 E✝
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E✝
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕝 E
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded (fun x => normSeminorm 𝕝 E) (fun i => q i) f
⊢ Continuous ↑f
𝕜 : Type ?u.658783
𝕜₂ : Type ?u.658786
𝕝 : Type u_2
𝕝₂ : Type u_4
E✝ : Type ?u.658795
F : Type u_3
G : Type ?u.658801
ι : Type u_5
ι' : Type ?u.658807
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E✝
inst✝¹⁵ : Module 𝕜 E✝
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E✝
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕝 E
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι), ∃ C, comp (q i) f ≤ C • normSeminorm 𝕝 E
⊢ Continuous ↑f
rw [← Seminorm.const_isBounded (Fin 1)] at hf
no goals
𝕜 : Type ?u.658783
𝕜₂ : Type ?u.658786
𝕝 : Type u_2
𝕝₂ : Type u_4
E✝ : Type ?u.658795
F : Type u_3
G : Type ?u.658801
ι : Type u_5
ι' : Type ?u.658807
inst✝¹⁷ : NontriviallyNormedField 𝕜
inst✝¹⁶ : AddCommGroup E✝
inst✝¹⁵ : Module 𝕜 E✝
inst✝¹⁴ : NormedField 𝕝
inst✝¹³ : Module 𝕝 E✝
inst✝¹² : NontriviallyNormedField 𝕜₂
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : NormedField 𝕝₂
inst✝⁸ : Module 𝕝₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : RingHomIsometric σ₁₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁶ : RingHomIsometric τ₁₂
inst✝⁵ : Nonempty ι
inst✝⁴ : Nonempty ι'
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕝 E
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
q : ι → Seminorm 𝕝₂ F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded (fun x => normSeminorm 𝕝 E) (fun i => q i) f
⊢ Continuous ↑f
exact continuous_from_bounded (norm_withSeminorms 𝕝 E) hq f hf