English
If a linear partial map f is closable and another partial map g satisfies g ≤ f, then g is closable as well.
Русский
Если частичное линейное отображение f дополняемо к замкнутому отображению и другое частичное отображение g удовлетворяет g ≤ f, то и g дополняемо к замкнутому отображению.
LaTeX
$$$ \\text{If } f \\text{ is closable and } g \\le f, \\text{ then } g \\text{ is closable. }$$$
Lean4
/-- If `g` has a closable extension `f`, then `g` itself is closable. -/
theorem leIsClosable {f g : E →ₗ.[R] F} (hf : f.IsClosable) (hfg : g ≤ f) : g.IsClosable :=
by
obtain ⟨f', hf⟩ := hf
have : g.graph.topologicalClosure ≤ f'.graph := by
rw [← hf]
exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)
use g.graph.topologicalClosure.toLinearPMap
rw [Submodule.toLinearPMap_graph_eq]
exact fun _ hx hx' => f'.graph_fst_eq_zero_snd (this hx) hx'
