toSubmodule_sSup

Mathlib.Topology.Algebra.Module.ClosedSubmodule

URI: https://scilib.ai/kg/mathlib#ClosedSubmodule.toSubmodule_sSup

English

The toSubmodule of the supremum over S is the closure of the supremum of the submodules.

Русский

toSubmodule(sSup S) равен замыканию_sup (s.toSubmodule).

LaTeX

$$$toSubmodule( sSup S ) = (\bigvee S \text{ in Submodule}).closure.toSubmodule$$$

Lean4

@[simp]
theorem toSubmodule_sSup (S : Set (ClosedSubmodule R N)) : toSubmodule (sSup S) = (⨆ s ∈ S, s.toSubmodule).closure :=
  rfl

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

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

Разделы

Аффилиация

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