inf — Mathlib

English

The infimum of a multiset is defined as the fold (inf) over the multiset starting from the top element: inf(s) = s.fold (⊓) ⊤.

Русский

Наименьшая грань мультимножества определяется как свёртка операции ∧ над элементами, начиная с верхнего элемента.

LaTeX

$$$$ \\mathrm{inf}(s) = s.fold(\\inf)\\top $$$$

Lean4

/-- Infimum of a multiset: `inf {a, b, c} = a ⊓ b ⊓ c` -/
def inf (s : Multiset α) : α :=
  s.fold (· ⊓ ·) ⊤

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