English
If f is invertible and closable, then the closure of the inverse equals the inverse of the closure.
Русский
Если f обратимо и замыкаемо, то замыкание обратного равно обратному замыканию.
LaTeX
$$$f.inverse.closure = f.closure.inverse$$$
Lean4
/-- Assuming that `f` is invertible and closable, then the closure is invertible if and only
if the inverse of `f` is closable. -/
theorem inverse_isClosable_iff (hf : LinearMap.ker f.toFun = ⊥) (hf' : f.IsClosable) :
f.inverse.IsClosable ↔ LinearMap.ker f.closure.toFun = ⊥ :=
by
constructor
· intro ⟨f', h⟩
rw [LinearMap.ker_eq_bot']
intro ⟨x, hx⟩ hx'
simp only [Submodule.mk_eq_zero]
rw [toFun_eq_coe, eq_comm, image_iff] at hx'
have : (0, x) ∈ graph f' := by
rw [← h, inverse_graph hf]
rw [← hf'.graph_closure_eq_closure_graph, ← SetLike.mem_coe, Submodule.topologicalClosure_coe] at hx'
apply image_closure_subset_closure_image continuous_swap
simp only [Set.mem_image, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
exact ⟨x, 0, hx', rfl, rfl⟩
exact graph_fst_eq_zero_snd f' this rfl
· intro h
use f.closure.inverse
exact (closure_inverse_graph hf hf' h).symm
