iInf₂ — Mathlib

English

If for all i and j the ideals f(i,j) are homogeneous, then their double infimum ⨅ i ⨅ j f(i,j) is homogeneous.

Русский

Если для всех i, j идеалы f(i,j) однородны, то их двойной нижний предел является однородным.

LaTeX

$$$(\\forall i, j, IsHomogeneous(\\mathcal{A}, f(i,j))) \\Rightarrow IsHomogeneous(\\mathcal{A}, \\bigsqcap_i \\bigsqcap_j f(i,j))$$$

Lean4

theorem iInf₂ {κ : Sort*} {κ' : κ → Sort*} {f : ∀ i, κ' i → Ideal A} (h : ∀ i j, (f i j).IsHomogeneous 𝒜) :
    (⨅ (i) (j), f i j).IsHomogeneous 𝒜 :=
  IsHomogeneous.iInf fun i => IsHomogeneous.iInf <| h i

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