𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1})
𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (polar B s)
rw [polar_eq_iInter]
𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
x✝ : x ∈ s
⊢ IsClosed {y | ‖↑(↑B x) y‖ ≤ 1}
𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1})
refine' isClosed_iInter fun x => isClosed_iInter fun _ => _
no goals
𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
x✝ : x ∈ s
⊢ IsClosed {y | ‖↑(↑B x) y‖ ≤ 1}
exact isClosed_le (WeakBilin.eval_continuous B.flip x).norm continuous_const