support_sup — Mathlib

English

The support of the supremum of two ideal data equals the intersection of supports: Supp(I ⊔ J) = Supp(I) ∩ Supp(J).

Русский

Поддержка объединения двух данных идеалов равна пересечению их поддержек.

LaTeX

$$ (I \\sqcup J).\\mathrm{support} = I.\\mathrm{support} \\cap J.\\mathrm{support} $$

Lean4

@[simp]
theorem support_sup (I J : X.IdealSheafData) : (I ⊔ J).support = I.support ⊓ J.support :=
  gc.l_sup

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