smul_iSup — Mathlib

English

Let I be a submodule of A and t: ι → submodules of M. Then I acts on the supremum of the t_i termwise: I • (⨆ i, t_i) = ⨆ i, I • t_i.

Русский

Пусть I — подмодуль A и t_i — подмодули M. Тогда действие on верхний предел распределяется по индексу: I • (⨆ i, t_i) = ⨆ i, I • t_i.

LaTeX

$$$ I \cdot (\bigvee_i t_i) = \bigvee_i (I \cdot t_i) $$$

Lean4

theorem smul_iSup {ι : Sort*} {I : Submodule R A} {t : ι → Submodule R M} : I • (⨆ i, t i) = ⨆ i, I • t i :=
  toAddSubmonoid_injective <| by simp only [smul_toAddSubmonoid, iSup_toAddSubmonoid, AddSubmonoid.smul_iSup]

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