inverse_closure — Mathlib

English

If hf and hcf hold (ker f = ⊥ and ker f.closure = ⊥), then f.closure.inverse = f.inverse.closure.

Русский

При выполнении условий на ядро замыкания и ядро обратного, графы обратных замыканий совпадают.

LaTeX

$$$hf \ \\text{and} \\ hcf \\Rightarrow f.closure.inverse = f.inverse.closure$$$

Lean4

/-- If `f` is invertible and closable, then taking the closure and the inverse commute. -/
theorem inverse_closure (hf : LinearMap.ker f.toFun = ⊥) (hf' : f.IsClosable)
    (hcf : LinearMap.ker f.closure.toFun = ⊥) : f.inverse.closure = f.closure.inverse :=
  by
  apply eq_of_eq_graph
  rw [closure_inverse_graph hf hf' hcf, ((inverse_isClosable_iff hf hf').mpr hcf).graph_closure_eq_closure_graph]

Похожие утверждения