Is Closable of continuous

lemma isClosable_of_continuous (h : Continuous U) : U.IsClosable := by  use U.graph.topologicalClosure.toLinearPMap  refine (toLinearPMap_graph_eq _ fun x hx hx₁ ↦ ?_).symm  obtain ⟨b, hb, hbx⟩ := mem_closure_iff_seq_limit.mp hx  rw [nhds_prod_eq] at hbx  refine norm_eq_zero.mp (tendsto_nhds_unique hbx.snd.norm ?_)  obtain ⟨M, hM, h_bound⟩ := LinearMap.continuous_iff_bounded.mp h  refine squeeze_zero (g := fun n ↦ M * ‖(b n).1‖) (fun _ ↦ norm_nonneg _) (fun n ↦ ?_) ?_  · obtain ⟨y, hy₁, hy₂⟩ := (mem_graph_iff _).mp (hb n)    simp only [← hy₁, ← hy₂]    exact h_bound y  · exact mul_zero M ▸ (norm_eq_zero.mpr hx₁) ▸ hbx.fst.norm.const_mul M