rothNumberNat_spec — Mathlib

English

There exists a subset t ⊆ {0,1,...,n−1} such that |t| = rothNumberNat(n) and ThreeAPFree(t).

Русский

Существует подмножество t ⊆ {0,1,...,n−1} такое, что |t| = rothNumberNat(n) и ThreeAPFree(t).

LaTeX

$$$\\exists t \\subseteq \\{0,1,\\dots,n-1\\},\\; |t| = \\operatorname{rothNumberNat}(n) \\land ThreeAPFree(t).$$$

Lean4

theorem rothNumberNat_spec (n : ℕ) : ∃ t ⊆ range n, #t = rothNumberNat n ∧ ThreeAPFree (t : Set ℕ) :=
  addRothNumber_spec _

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