completeLattice — Mathlib

English

There is a complete lattice structure on the set of partitions of α, under the refinement order.

Русский

Для множества разбиений α существует структура полного решета под упорядочением по уточнению.

LaTeX

$$$\\text{CompleteLattice}(\\text{Subtype}\\; \\text{IsPartition } α)$$$

Lean4

/-- A complete lattice instance for partitions; there is more infrastructure for the
equivalent complete lattice on equivalence relations. -/
instance completeLattice : CompleteLattice (Subtype (@IsPartition α)) :=
  GaloisInsertion.liftCompleteLattice <|
    @OrderIso.toGaloisInsertion _ (Subtype (@IsPartition α)) _ (PartialOrder.toPreorder) <| Partition.orderIso α

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