isClosable

Mathlib.Topology.Algebra.Module.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearPMap.IsClosed.isClosable

← MathLib Explorer

English

If f is closable and g ≤ f, then g is closable as well.

Русский

Если f близко продолжимо и g ≤ f, то и g также близко продолжимо.

LaTeX

$$$$ \text{If } f \text{ is closable and } g \le f, \text{ then } g \text{ is closable.} $$$$

Lean4

/-- A closed operator is trivially closable. -/
theorem isClosable {f : E →ₗ.[R] F} (hf : f.IsClosed) : f.IsClosable :=
  ⟨f, hf.submodule_topologicalClosure_eq⟩

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

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

Разделы

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

Аффилиация

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