instMin — Mathlib

English

For a family of ideals f i, if each f i is homogeneous, then the infimum ⨅ i f i is homogeneous.

Русский

Для семейства идеалов f_i, если каждый f_i однороден, то их инфимум ⨅ i f_i однороден.

LaTeX

$$$(\\forall i, IsHomogeneous(\\mathcal{A}, f(i))) \\Rightarrow IsHomogeneous(\\mathcal{A}, \\big(\\bigwedge_i f(i)\\big))$$$

Lean4

instance : Min (HomogeneousIdeal 𝒜) :=
  ⟨fun I J => ⟨_, I.isHomogeneous.inf J.isHomogeneous⟩⟩

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