instSupSet — Mathlib

English

SupSet over a family of closed submodules is the closure of the supremum of their underlying submodules.

Русский

SupSet для семейства замкнутых подмодулей равен замыканию супа соответствующих подмодулей.

LaTeX

$$$\operatorname{SupSet}(S) = \langle (\bigvee_{s\in S} s.toSubmodule).closure, \text{isClosed_closure} \rangle$$$

Lean4

instance : SupSet (ClosedSubmodule R N) where sSup S := ⟨(⨆ s ∈ S, s.toSubmodule).closure, isClosed_closure⟩

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