[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ UniformSpace.toTopologicalSpace ≤ WeakDual.instTopologicalSpace
[PROOFSTEP]
convert (@toWeakDual_continuous _ _ _ _ (by assumption)).le_induced
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ NormedSpace 𝕜 E
[PROOFSTEP]
assumption
[GOAL]
case h.e'_4
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ WeakDual.instTopologicalSpace = TopologicalSpace.induced (fun x' => ↑toWeakDual x') WeakDual.instTopologicalSpace
[PROOFSTEP]
exact induced_id.symm
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (polar 𝕜 s)
[PROOFSTEP]
simp only [polar_def, setOf_forall]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ (i : E) (_ : i ∈ s), {x | ‖↑x i‖ ≤ 1})
[PROOFSTEP]
exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm
