instLattice — Mathlib

English

The collection of multisets is equipped with a lattice structure where join is union and meet is intersection.

Русский

Множество мультимножество образует решётку, где объединение выступает как сосуществование (верхняя граница), а пересечение — как Meet (нижняя граница).

LaTeX

$$$\\text{There is a lattice structure on } \\mathrm{Multiset}(\\alpha)\\text{ with } \\sup = \\cup, \\inf = \\cap.$$$

Lean4

instance instLattice : Lattice (Multiset α) where
  sup := (· ∪ ·)
  sup_le _ _ _ := union_le
  le_sup_left _ _ := le_union_left
  le_sup_right _ _ := le_union_right
  inf := (· ∩ ·)
  le_inf _ _ _ := le_inter
  inf_le_left _ _ := inter_le_left
  inf_le_right _ _ := inter_le_right

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