iInf_toSubmodule — Mathlib

English

The underlying Submodule of the infimum of a family of Subalgebras equals the infimum of the corresponding Submodules: toSubmodule(iInf S) = ⨅ i, toSubmodule (S i).

Русский

Основное подмодульное множество пересечения семейства подпалгебр равно инфимума соответствующих подмодулей: toSubmodule(iInf S) = ⨅ i, toSubmodule(S i).

LaTeX

$$$\operatorname{toSubmodule}(\bigwedge_i S_i) = \bigwedge_i \operatorname{toSubmodule}(S_i)$$$

Lean4

@[simp]
theorem iInf_toSubmodule {ι : Sort*} (S : ι → Subalgebra R A) : toSubmodule (⨅ i, S i) = ⨅ i, toSubmodule (S i) :=
  SetLike.coe_injective <| by simp

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