no goals
𝕜₁ : Type u_3
𝕜₂ : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜₁
inst✝⁶ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_4
M₂ : Type u_2
M₃ : Type ?u.72218
inst✝⁵ : SeminormedAddCommGroup M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : NormedSpace 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ↑f
S : Set M₁
hS : Metric.Bounded S
⊢ IsVonNBounded 𝕜₁ S
rwa [NormedSpace.isVonNBounded_iff, ← Metric.bounded_iff_isBounded]