instSupSet — Mathlib

English

If every f i j is homogeneous, then the double supremum ⨆ 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}, \\bigsqcup_i \\bigsqcup_j f(i,j))$$$

Lean4

instance : SupSet (HomogeneousIdeal 𝒜) :=
  ⟨fun S => ⟨⨆ s ∈ S, toIdeal s, Ideal.IsHomogeneous.iSup₂ fun s _ => s.isHomogeneous⟩⟩

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