toIdeal_iInf — Mathlib

English

Let 𝒜 be a graded ring and {s_i}_{i ∈ κ} a family of homogeneous ideals of 𝒜. Then the ideal associated to the infimum of the family equals the infimum of the associated ideals: (⨅ i, s_i).toIdeal = ⨅ i, (s_i).toIdeal.

Русский

Пусть 𝒜 — градуированное кольцо и {s_i}_{i ∈ κ} — множество однородных идеалов 𝒜. Тогда идеал, соответствующий наименьшему пределу семейства, равен наименьшему пределу образов: (⨅ i, s_i).toIdeal = ⨅ i, (s_i).toIdeal.

LaTeX

$$$ (\inf_i s(i)).toIdeal = \inf_i (s(i).toIdeal) $$$

Lean4

@[simp]
theorem toIdeal_iInf {κ : Sort*} (s : κ → HomogeneousIdeal 𝒜) : (⨅ i, s i).toIdeal = ⨅ i, (s i).toIdeal := by
  rw [iInf, toIdeal_sInf, iInf_range]

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