sInf_toSubmodule — Mathlib

English

The sInf of a set S of LieSubmodules, when mapped to Submodule, equals the intersection of their underlying Submodules.

Русский

Обобщённый нижний предел множества подмодулей Lie, приводимый к Submodule, равен пересечению их подмодулей.

LaTeX

$$$ (\text{LieSubmodule}.instInfSet.sInf S).toSubmodule = \bigcap_{N \in S} N^{toSubmodule} $$$

Lean4

@[simp]
theorem sInf_toSubmodule (S : Set (LieSubmodule R L M)) :
    (↑(sInf S) : Submodule R M) = sInf ({(s : Submodule R M) | s ∈ S}) :=
  rfl

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