iInf_toSubmodule — Mathlib

English

For any family p:ι → LieSubmodule R L M, the Submodule underlying iInf p equals the iInf of the underlying Submodules.

Русский

Для любой семьи p:ι → LieSubmodule R L M подмодуль, лежащий в основе iInf p, равен iInf от подмодулей p(i).

LaTeX

$$$ (iInf \ f)^{toSubmodule} = iInf (f \toSubmodule) $$$

Lean4

@[simp]
theorem iInf_toSubmodule {ι} (p : ι → LieSubmodule R L M) :
    (↑(⨅ i, p i) : Submodule R M) = ⨅ i, (p i : Submodule R M) := by rw [iInf, sInf_toSubmodule]; ext; simp

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