support_iSup — Mathlib

English

The support of the supremum of a family equals the infimum of the supports: Supp( iSup I ) = ⨅ i, Supp(I_i).

Русский

Поддержка супремума семейства равна инфимума поддержек его членов.

LaTeX

$$(\\mathrm{iSup}\\,I).\\mathrm{support} = \\bigwedge_i (I_i).\\mathrm{support}$$

Lean4

@[simp]
theorem support_iSup {ι : Sort*} (I : ι → X.IdealSheafData) : (iSup I).support = ⨅ i, (I i).support :=
  gc.l_iSup

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