𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (LinearMap.polar (LinearMap.flip (dualPairing 𝕜 E)) s)
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (polar 𝕜 s)
dsimp only [NormedSpace.polar]
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑(dualPairing 𝕜 E) y) x‖ ≤ 1})
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (LinearMap.polar (LinearMap.flip (dualPairing 𝕜 E)) s)
simp only [LinearMap.polar_eq_iInter, LinearMap.flip_apply]
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
z : E
x✝ : z ∈ s
⊢ IsClosed {y | ‖↑(↑(dualPairing 𝕜 E) y) z‖ ≤ 1}
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑(dualPairing 𝕜 E) y) x‖ ≤ 1})
refine' isClosed_biInter fun z _ => _
no goals
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
z : E
x✝ : z ∈ s
⊢ IsClosed {y | ‖↑(↑(dualPairing 𝕜 E) y) z‖ ≤ 1}
exact isClosed_Iic.preimage (ContinuousLinearMap.apply 𝕜 𝕜 z).continuous.norm