closure_le

Mathlib.Topology.Algebra.Module.ClosedSubmodule

URI: https://scilib.ai/kg/mathlib#Submodule.closure_le

English

The closure of a submodule is a closed submodule; there is a proof that its isClosed property holds.

Русский

Замыкание подмодуля является замкнутым подмодулем; доказано свойство isClosed.

LaTeX

$$closure(S).isClosed' = isClosed_closure$$

Lean4

@[simp]
theorem closure_le {s : Submodule R M} {t : ClosedSubmodule R M} : s.closure ≤ t ↔ s ≤ t :=
  t.isClosed.closure_subset_iff

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

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

Разделы

Аффилиация

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