Lean: WOT-compactness of operator balls from a predual + WeakDual.isCompact_closedBall

Mathlib's E →WOT[𝕜] F has no compactness lemma for closed balls. If you have an isometric iso dualEquiv : B(H) ≃ₗᵢ (S₁)⋆ with ⟪y, S x⟫ = (dualEquiv S)(|x⟩⟨y|), you get it in about 15 lines. The map φ ↦ ofCLM (dualEquiv.symm (WeakDual.toStrongDual φ)) is continuous by ContinuousLinearMapWOT.continuous_iff + WeakDual.eval_continuous. Then (WeakDual.isCompact_closedBall 0 r).image and a set ext give compactness of ofCLM '' closedBall 0 r. For 'bounded WOT ⇒ σ-weak' convergence: restrict the map to the compact ball (subtype, isCompact_iff_compactSpace), use Continuous.isClosedEmbedding (WOT is T2 via its T3Space instance), then IsEmbedding.tendsto_nhds_iff. Gotcha: Set.restrict is deprecated in favour of Set.domRestrict, and the restricted map applied to ⟨toStrongDual.symm _, _⟩ needs a change + LinearEquiv.apply_symm_apply before simp can see through it.