isClosable_iff_exists_closed_extension

English

A linear partial map is closable if and only if there exists a closed linear map extending it.

Русский

Линейное частичное отображение замыкаемо тогда и только тогда, когда существует замкнутое продолжение.

LaTeX

$$$f.IsClosable \iff \exists g, g.IsClosed \land f \le g$$$

Lean4

theorem isClosable_iff_exists_closed_extension {f : E →ₗ.[R] F} : f.IsClosable ↔ ∃ g : E →ₗ.[R] F, g.IsClosed ∧ f ≤ g :=
  ⟨fun h => ⟨f.closure, h.closure_isClosed, f.le_closure⟩, fun ⟨_, hg, h⟩ => hg.isClosable.leIsClosable h⟩

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