IsClosable — Mathlib

English

An operator is closable if there exists some extension whose graph matches the closure of its graph.

Русский

Оператор близко продолжим, если существует расширение, график которого совпадает с замыканием графика оператора.

LaTeX

$$$$ \text{IsClosable}(f) \;\equiv\; \exists f' : \text{LinearPMap}, \ \mathrm{graph}(f)_{\text{top. closure}} = \mathrm{graph}(f') $$$$

Lean4

/-- An unbounded operator is closable iff the closure of its graph is a graph. -/
def IsClosable (f : E →ₗ.[R] F) : Prop :=
  ∃ f' : LinearPMap R E F, f.graph.topologicalClosure = f'.graph

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