closure_isClosed

Mathlib.Topology.Algebra.Module.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearPMap.IsClosable.closure_isClosed

← MathLib Explorer

English

If f is closable, then f.closure is a closed submodule.

Русский

Если f замыкаемо, то f.closure является замкнутым подпредметом.

LaTeX

$$$f.Closure.IsClosed$$$

Lean4

/-- If `f` is closable, then the closure is closed. -/
theorem closure_isClosed {f : E →ₗ.[R] F} (hf : f.IsClosable) : f.closure.IsClosed :=
  by
  rw [IsClosed, ← hf.graph_closure_eq_closure_graph]
  exact f.graph.isClosed_topologicalClosure

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru