iSup_eq_span — Mathlib

English

The supremum of a family of submodules equals the span of the union of the underlying sets: ⨆ i, p_i = span_R(⋃ i, ↑(p_i)).

Русский

Супремум семейства подмодулей равен линейной оболочке объединения базовых множеств: ⨆ i, p_i = span_R(⋃ i, ↑(p_i)).

LaTeX

$$$\big\vee_i p_i = \operatorname{span}_R\left(\bigcup_i \uparrow(p_i)\right)$$$

Lean4

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

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