instInfSet — Mathlib

English

For any set S of closed submodules of M, the infimum sInf S exists and is the closed submodule whose underlying submodule is the intersection of all s.toSubmodule for s ∈ S.

Русский

Для любого множества S замкнутых подмодулей M существует инфимума (sInf S); его базовый подмодуль равен пересечению всех s.toSubmodule по s ∈ S.

LaTeX

$$$\operatorname{toSubmodule}(\mathrm{sInf}(S)) = \bigwedge_{s \in S} s.toSubmodule$$

Lean4

instance instInfSet : InfSet (ClosedSubmodule R M) where
  sInf S := ⟨⨅ s ∈ S, s, by simpa using isClosed_biInter fun x hx ↦ x.isClosed⟩

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