sInf_toSubmodule_eq_iInf — Mathlib

English

The Submodule underlying sInf S equals the iInf of the submodules corresponding to S.

Русский

Основанный Submodule нижнего предела S равен iInf от подмодулей, соответствующих элементам S.

LaTeX

$$$ (\text{instInfSet}.sInf S).toSubmodule = \inf_{N\in S} (N.toSubmodule) $$$

Lean4

theorem sInf_toSubmodule_eq_iInf (S : Set (LieSubmodule R L M)) :
    (↑(sInf S) : Submodule R M) = ⨅ N ∈ S, (N : Submodule R M) := by rw [sInf_toSubmodule, ← Set.image, sInf_image]

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