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
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ UniformSpace.toTopologicalSpace ≤ WeakDual.instTopologicalSpace
convert (@toWeakDual_continuous _ _ _ _ (by assumption)).le_induced
no goals
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
exact induced_id.symm
no goals
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ NormedSpace 𝕜 E
assumption