English
If f is closable and invertible with closed inverse, then the graph of the inverse of f.closure equals the closure of the graph of the inverse.
Русский
Если f замыкаемо и обратное к f замкнуто, то граф обратной к замыканию совпадает с замыканием графа обратного.
LaTeX
$$$f.graph.topologicalClosure = f.closure.graph$ inverse relation$$$
Lean4
/-- If `f` is invertible and closable as well as its closure being invertible, then
the graph of the inverse of the closure is given by the closure of the graph of the inverse. -/
theorem closure_inverse_graph (hf : LinearMap.ker f.toFun = ⊥) (hf' : f.IsClosable)
(hcf : LinearMap.ker f.closure.toFun = ⊥) : f.closure.inverse.graph = f.inverse.graph.topologicalClosure :=
by
rw [inverse_graph hf, inverse_graph hcf, ← hf'.graph_closure_eq_closure_graph]
apply SetLike.ext'
simp only [Submodule.topologicalClosure_coe, Submodule.map_coe, LinearEquiv.prodComm_apply]
apply (image_closure_subset_closure_image continuous_swap).antisymm
have h1 := Set.image_equiv_eq_preimage_symm f.graph (LinearEquiv.prodComm R E F).toEquiv
have h2 := Set.image_equiv_eq_preimage_symm (_root_.closure f.graph) (LinearEquiv.prodComm R E F).toEquiv
simp only [LinearEquiv.coe_toEquiv, LinearEquiv.prodComm_apply] at h1 h2
rw [h1, h2]
apply continuous_swap.closure_preimage_subset
