iSup_eq_span — Mathlib

English

The supremum of a family of ideals equals the span of the union of their underlying sets: ⨆ i, p(i) = span(⋃ i, ↑(p(i))).

Русский

Наибольший элемент множества идеалов равен порождению множества их оснований: ⨆ i, p(i) = span(⋃ i, ↑(p(i))).

LaTeX

$$$\\bigvee_{i} p(i) = \\operatorname{span}\\Big(\\bigcup_{i} \\uparrow p(i)\\Big)$$$

Lean4

theorem iSup_eq_span {ι} (p : ι → Ideal α) : ⨆ i, p i = span (⋃ i, ↑(p i)) :=
  Submodule.iSup_eq_span p

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