Erdős problem 624

Let $X$ be a finite set of size $n$ and $H(n)$ be such that there is a function $f:\{A : A\subseteq X\}\to X$ so that for every $Y\subseteq X$ with $\lvert Y\rvert \geq H(n)$ we have $\left\{ f(A) : A\subseteq Y\right\}=X$ . Prove that $H(n)-\log_2 n \to \infty$ .

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

624.lean

Retained formal statement1 of 1

Let $X$ be a finite set of size $n$ and $H(n)$ be such that there is a function $f:\{A : A\subseteq X\}\to X$ so that for every $Y\subseteq X$ with $\lvert Y\rvert \geq H(n)$ we have $\left\{ f(A) : A\subseteq Y\right\}=X$ . Prove that $H(n)-\log_2 n \to \infty$ .

FormalConjectures/ErdosProblems/624.leanErdos624.erdos_6241 lineExact file

1Filter.Tendsto (fun n => ↑(Erdos624.H n) - Real.logb 2 ↑n) Filter.atTop Filter.atTop

OpenStatement only, no proof