sInf_toSubmodule — Mathlib

English

The Submodule underlying the infimum of a set S of Subalgebras equals the infimum of the images under toSubmodule: Subalgebra.toSubmodule(sInf S) = sInf (Subalgebra.toSubmodule '' S).

Русский

Подмодульная часть пересечения подпалгебр равна нижнему пределу образов подмодуля через toSubmodule: Subalgebra.toSubmodule(sInf S) = sInf (toSubmodule '' S).

LaTeX

$$$\operatorname{toSubmodule}(sInf S) = sInf(\operatorname{toSubmodule}''S)$$$

Lean4

@[simp]
theorem sInf_toSubmodule (S : Set (Subalgebra R A)) :
    Subalgebra.toSubmodule (sInf S) = sInf (Subalgebra.toSubmodule '' S) :=
  SetLike.coe_injective <| by simp

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