English
A Frobenius number n for a set s is the largest n such that n is not in the additive closure of s, and every larger integer is in that closure.
Русский
Число Фробениуса n относительно множества s есть наибольшее n, не принадлежащее суммарной полугруппе, образованной s, причём каждый больший чем n целый число принадлежит этой замкнутости.
LaTeX
$$$\\mathrm{FrobeniusNumber}(n,s) \\iff n \\notin \\mathrm{AddSubmonoid.closure}(s) \\land \\forall k > n,\\; k \\in \\mathrm{AddSubmonoid.closure}(s)$$$
Lean4
theorem frobeniusNumber_iff {n : ℕ} {s : Set ℕ} :
FrobeniusNumber n s ↔ n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s := by
simp_rw [FrobeniusNumber, IsGreatest, upperBounds, Set.mem_setOf, not_imp_comm, not_le]
