English
For a set s of natural numbers, a Frobenius number n is the largest natural number not expressible as a nonnegative integer combination of elements of s.
Русский
Для множества натуральных чисел s число Фробениуса n — наибольшее натуральное число, которое не выражается как неотрицательная линейная комбинация элементов s.
LaTeX
$$$\\mathrm{FrobeniusNumber}(n,s) \\iff n \\notin \\mathrm{AddSubmonoid.closure}(s) \\land \\forall k>n\\, (k \\in \\mathrm{AddSubmonoid.closure}(s))$$$
Lean4
/-- A natural number `n` is the **Frobenius number** of a set of natural numbers `s` if it is an
upper bound on the complement of the additive submonoid generated by `s`.
In other words, it is the largest number that cannot be expressed as a sum of numbers in `s`. -/
def FrobeniusNumber (n : ℕ) (s : Set ℕ) : Prop :=
IsGreatest {k | k ∉ AddSubmonoid.closure s} n
