English
The closure of a linear partial map f is defined as the unique closed extension if f is closable, and equals f otherwise.
Русский
Замыкание линейного частичного отображения f определяется как единственное замкнутое продолжение, если f замыкаемо, и иначе как само f.
LaTeX
$$$\\\\mathrm{closure}(f) = \\\\begin{cases} \\\\text{the unique } f' \\\\text{ with } f'.graph = \overline{f.graph}, & f \\\\text{is closable} \\\\newline \\\\text{and}\\ f'.graph = \overline{f.graph} \\\\\\\\ \\\\text{else} \\\\ \\\\ f, \\\\end{cases}$$$
Lean4
/-- If `f` is closable, then `f.closure` is the closure. Otherwise it is defined
as `f.closure = f`. -/
noncomputable def closure (f : E →ₗ.[R] F) : E →ₗ.[R] F :=
if hf : f.IsClosable then hf.choose else f
