instInfSet — Mathlib

English

If every f i j is homogeneous, then the double infimum ⨅ i ⨅ j f i j is homogeneous.

Русский

Если каждый f_{i,j} однороден, то двойной инфимум по i и j однороден.

LaTeX

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

Lean4

instance : InfSet (HomogeneousIdeal 𝒜) :=
  ⟨fun S => ⟨⨅ s ∈ S, toIdeal s, Ideal.IsHomogeneous.iInf₂ fun s _ => s.isHomogeneous⟩⟩

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