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

Open selected source

FormalConjectures/ErdosProblems/

168.lean

Retained formal statement8 of 9

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

FormalConjectures/ErdosProblems/168.leanErdos168.F_eq_card4 linesExact file

1∀ (N : ℕ),2  ∀ S ⊆ Finset.Icc 1 N,3    Erdos168.NonTernary S →4      (∀ T ⊆ Finset.Icc 1 N, Erdos168.NonTernary T → S.card ≤ T.card → T.card = S.card) → Erdos168.F N = S.card

APIStatement only, no proof

Sources

Search problems.science