instMax — Mathlib

English

The maximum of two homogeneous ideals (with respect to inclusion) is again homogeneous.

Русский

Наибольший элемент двух однородных идеалов по включению снова однороден.

LaTeX

$$$\\text{IsHomogeneous}(\\mathcal{A}, I) \\land \\text{IsHomogeneous}(\\mathcal{A}, J) \\Rightarrow \\text{IsHomogeneous}(\\mathcal{A}, \\max(I,J))$$$

Lean4

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

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