no goals
𝕜 : Type u_2
𝕜₂ : Type u_4
𝕝 : Type ?u.110955
𝕝₂ : Type ?u.110958
E : Type u_3
F : Type u_5
G : Type ?u.110967
ι : Type u_6
ι'✝ : Type ?u.110973
inst✝⁷ : NormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : NormedField 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι' : Type u_1
inst✝ : Nonempty ι'
p : ι → Seminorm 𝕜 E
q : Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
⊢ IsBounded p (fun x => q) f ↔ ∃ s C, comp q f ≤ C • Finset.sup s p
simp only [IsBounded, forall_const]