toIdeal_sInf — Mathlib

English

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

Русский

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

LaTeX

$$$(\\text{toIdeal\_sInf})\\;: \\forall \\mathcal{I}, (sInf \\mathcal{I}).toIdeal = \\bigsqcap_{s \\in \\mathcal{I}} s.toIdeal$$$

Lean4

@[simp]
theorem toIdeal_sInf (ℐ : Set (HomogeneousIdeal 𝒜)) : (sInf ℐ).toIdeal = ⨅ s ∈ ℐ, toIdeal s :=
  rfl

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