English
Let 𝒜 be a graded ring and s : ∀ i, κ' i → HomogeneousIdeal 𝒜. Then the supremum 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( \big\l updownarrow \; \big( \sup_{i} \sup_{j} s(i,j) \big) \Big).toIdeal = \sup_{i} \sup_{j} (s(i,j).toIdeal) $$$$
Lean4
theorem toIdeal_iSup₂ {κ : Sort*} {κ' : κ → Sort*} (s : ∀ i, κ' i → HomogeneousIdeal 𝒜) :
(⨆ (i) (j), s i j).toIdeal = ⨆ (i) (j), (s i j).toIdeal := by simp_rw [toIdeal_iSup]
