𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ (i : E) (_ : i ∈ s), {x | ‖↑x i‖ ≤ 1})
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (polar 𝕜 s)
simp only [polar_def, setOf_forall]
no goals
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ (i : E) (_ : i ∈ s), {x | ‖↑x i‖ ≤ 1})
exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm