Erdős problem 770

For odd `n`, the values of `h n` form an unbounded set. This is described as 'easy to see' in [Er74b].

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

770.lean

Retained formal statement4 of 6

For odd n, the values of h n form an unbounded set. This is described as 'easy to see' in [Er74b].

FormalConjectures/ErdosProblems/770.leanErdos770.erdos_770.variants.odd_h_unbounded1 lineExact file

1Set.Unbounded (fun x1 x2 => x1 ≤ x2) (ENat.toNat '' (Erdos770.h '' Odd))

TextbookStatement only, no proof