toIdeal_iInf₂ — Mathlib

English

Let 𝒜 be a graded ring and s : ∀ i, κ' i → HomogeneousIdeal 𝒜. Then the infimum over the double index (i, j) commutes with taking toIdeal: (⨅ i (j), s i j).toIdeal = ⨅ i (j), (s i j).toIdeal.

Русский

Пусть 𝒜 — градуированное кольцо и s : ∀ i, κ'(i) → HomogeneousIdeal 𝒜. Тогда инфимум по двойному индексу (i, j) и последующее применение toIdeal равняется инфимуму по каждому индексу: (⨅ i (j), s i j).toIdeal = ⨅ i (j), (s i j).toIdeal.

LaTeX

$$$ \Big( \inf_{i} \inf_{j} s(i,j) \Big).toIdeal = \inf_{i} \inf_{j} (s(i,j).toIdeal) $$$

Lean4

theorem toIdeal_iInf₂ {κ : Sort*} {κ' : κ → Sort*} (s : ∀ i, κ' i → HomogeneousIdeal 𝒜) :
    (⨅ (i) (j), s i j).toIdeal = ⨅ (i) (j), (s i j).toIdeal := by simp_rw [toIdeal_iInf]

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