𝕜 : Type ?u.643524
𝕜₂ : Type ?u.643527
𝕝 : Type u_4
𝕝₂ : Type u_2
E : Type u_3
F✝ : Type ?u.643539
G : Type ?u.643542
ι : Type u_5
ι' : Type ?u.643548
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 ι'
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕝₂ F
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : ι → Seminorm 𝕝 E
hp : WithSeminorms p
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p (fun x => normSeminorm 𝕝₂ F) f
⊢ Continuous ↑f
𝕜 : Type ?u.643524
𝕜₂ : Type ?u.643527
𝕝 : Type u_4
𝕝₂ : Type u_2
E : Type u_3
F✝ : Type ?u.643539
G : Type ?u.643542
ι : Type u_5
ι' : Type ?u.643548
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 ι'
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕝₂ F
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : ι → Seminorm 𝕝 E
hp : WithSeminorms p
f : E →ₛₗ[τ₁₂] F
hf : ∃ s C, comp (normSeminorm 𝕝₂ F) f ≤ C • Finset.sup s p
⊢ Continuous ↑f
rw [← Seminorm.isBounded_const (Fin 1)] at hf
no goals
𝕜 : Type ?u.643524
𝕜₂ : Type ?u.643527
𝕝 : Type u_4
𝕝₂ : Type u_2
E : Type u_3
F✝ : Type ?u.643539
G : Type ?u.643542
ι : Type u_5
ι' : Type ?u.643548
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 ι'
F : Type u_1
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕝₂ F
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : ι → Seminorm 𝕝 E
hp : WithSeminorms p
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p (fun x => normSeminorm 𝕝₂ F) f
⊢ Continuous ↑f
exact continuous_from_bounded hp (norm_withSeminorms 𝕝₂ F) f hf