Erdős problem 168 · problems.science

Sanity check: if S is a maximal non ternary subset of {1,..., N} then F N is given by the cardinality of S

Sources

Browse retained paths and inspect the exact material available for this Problem.

9 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

168.lean

Retained formal statement9 of 9

Sanity check: elements of IntervalNonTernarySets N are precisely non ternary subsets of {1,...,N}

FormalConjectures/ErdosProblems/168.leanErdos168.mem_IntervalNonTernarySets_iff1 lineExact file

1∀ (N : ℕ) (S : Finset ℕ), S ∈ Erdos168.IntervalNonTernarySets N ↔ Erdos168.NonTernary S ∧ S ⊆ Finset.Icc 1 N

APIStatement only, no proof