iSup_eq_span' — Mathlib

English

For a family p: ι → Submodule, the supremum of p equals the span of the union over i of p(i).

Русский

Для семейства p: ι → подмодуль, верхний предел p равен линейной оболочке объединения p(i) по всем i.

LaTeX

$$$\displaystyle \big\|\!\!\!_i p_i \!\!\| \_? = \operatorname{span}_R(\bigcup_i \uparrow(p_i))$$$

Lean4

theorem iSup_eq_span' {ι : Sort*} (p : ι → Submodule R M) (h : ι → Prop) :
    (⨆ (i : ι) (_ : h i), p i) = Submodule.span R (⋃ (i : ι) (_ : h i), ↑(p i)) := by
  simp_rw [← Submodule.iSup_span, Submodule.span_eq]

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