ideal_iSup — Mathlib

English

The ideal of the supremum over a family I is the supremum of the ideals pointwise.

Русский

Идеал наибольшего элемента семейства I равен точечному наибольшему среди их идеалов.

LaTeX

$$$ (\mathrm{iSup} I).ideal = \bigl( \bigvee_i I(i).ideal \bigr) $$$

Lean4

@[simp]
theorem ideal_iSup {ι : Type*} {I : ι → IdealSheafData X} : (iSup I).ideal = ⨆ i, (I i).ideal := by
  rw [← sSup_range, ← sSup_range, ideal_sSup, ← Set.range_comp, Function.comp_def]

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