sup — Mathlib

English

The supremum of a multiset is defined by folding with the join operation starting from the bottom element: sup(s) = fold(⊔) ⊥ s.

Русский

Наибольшее значение мультсета определяется как свёртка по операции объединения с нижней границей.

LaTeX

$$$\\operatorname{sup}(s) = \\operatorname{fold}(\\;\\cdot \\;\\,\\text{⊔} , \\bot, s)$$$

Lean4

/-- Supremum of a multiset: `sup {a, b, c} = a ⊔ b ⊔ c` -/
def sup (s : Multiset α) : α :=
  s.fold (· ⊔ ·) ⊥

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