completeLattice — Mathlib

English

The collection of homogeneous ideals of 𝒜 forms a complete lattice under inclusion, with the lattice operations induced from the corresponding operations on ideals.

Русский

Множество однородных идеалов 𝒜 образует полную решётку по включению, операции над ней соответствуют аналогичным операциям над идеалами.

LaTeX

$$$\text{HomogeneousIdeal } 𝒜 \text{ forms a complete lattice under inclusion, induced by the underlying ideal operations.}$$$

Lean4

instance completeLattice : CompleteLattice (HomogeneousIdeal 𝒜) :=
  toIdeal_injective.completeLattice _ toIdeal_sup toIdeal_inf toIdeal_sSup toIdeal_sInf toIdeal_top toIdeal_bot

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