English
Let f be a closable linear partial map. Then there exists a unique closed extension f' whose graph is the topological closure of the graph of f; equivalently, the graph of f' equals the topological closure of the graph of f.
Русский
Пусть f — замыкаемая линейная частичная отображение. Тогда существует единственное замкнутое продолжение f', граф которого равен топологическому замыканию графа f; эквивалентно, граф f' совпадает с замыканием графа f.
LaTeX
$$$\\exists! f' : E \\rightarrow_{R} F,\\; f.graph.topologicalClosure = f'.graph$$$
Lean4
/-- The closure is unique. -/
theorem existsUnique {f : E →ₗ.[R] F} (hf : f.IsClosable) : ∃! f' : E →ₗ.[R] F, f.graph.topologicalClosure = f'.graph :=
by
refine existsUnique_of_exists_of_unique hf fun _ _ hy₁ hy₂ => eq_of_eq_graph ?_
rw [← hy₁, ← hy₂]
