inf_toSubmodule — Mathlib

English

For any set S of Lie subalgebras, the underlying submodule of their infimum equals the infimum of the corresponding submodules.

Русский

Для множества S подалгебр Ли совпадает подмодуль инфимума S с инфимумом соответствующих подмодулей.

LaTeX

$$$ (↑(sInf S) : Submodule R L) = sInf ({(s : Submodule R L) | s ∈ S})$$$

Lean4

@[simp]
theorem inf_toSubmodule : (↑(K ⊓ K') : Submodule R L) = (K : Submodule R L) ⊓ (K' : Submodule R L) :=
  rfl

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