graph_closure_eq_closure_graph — Mathlib

English

For a closable f, the topological closure of its graph equals the graph of its closure.

Русский

Для замыкаемого f топологическое замыкание графа равно графу замыкания.

LaTeX

$$$f.graph.topologicalClosure = f.closure.graph$$$

Lean4

/-- The closure (as a submodule) of the graph is equal to the graph of the closure
  (as a `LinearPMap`). -/
theorem graph_closure_eq_closure_graph {f : E →ₗ.[R] F} (hf : f.IsClosable) :
    f.graph.topologicalClosure = f.closure.graph :=
  by
  rw [closure_def hf]
  exact hf.choose_spec

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