toIdeal_sSup — Mathlib

English

The toIdeal map sends the supremum of a set of homogeneous ideals to the supremum of their images.

Русский

Отображение toIdeal отправляет верхнюю границу множества однородных идеалов в верхнюю границу их изображений.

LaTeX

$$$(\\text{toIdeal\_sSup})\\;: \\forall \\mathcal{I}, (sSup \\mathcal{I}).toIdeal = \\bigsqcup_{s \\in \\mathcal{I}} s.toIdeal$$$

Lean4

@[simp]
theorem toIdeal_sSup (ℐ : Set (HomogeneousIdeal 𝒜)) : (sSup ℐ).toIdeal = ⨆ s ∈ ℐ, toIdeal s :=
  rfl

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