le_rothNumberNat — Mathlib

English

If s is ThreeAPFree ⊆ {0,1,...,n−1} with |s| = k, then k ≤ rothNumberNat(n).

Русский

Если s ⊆ {0,1,...,n−1} и ThreeAPFree(s) и |s| = k, то k ≤ rothNumberNat(n).

LaTeX

$$$\\forall s\\subseteq\\{0,1,\\dots,n-1\\},\\ ThreeAPFree(s) \\Rightarrow |s| \\le \\operatorname{rothNumberNat}(n).$$$

Lean4

/-- A verbose specialization of `threeAPFree.le_addRothNumber`, sometimes convenient in
practice. -/
theorem le_rothNumberNat (s : Finset ℕ) (hs : ThreeAPFree (s : Set ℕ)) (hsn : ∀ x ∈ s, x < n) (hsk : #s = k) :
    k ≤ rothNumberNat n :=
  hsk.ge.trans <| hs.le_addRothNumber fun x hx => mem_range.2 <| hsn x hx

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