Skip to content

Erdős problem 624

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

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

624.lean

Retained formal statement1 of 1

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

FormalConjectures/ErdosProblems/624.leanErdos624.erdos_6241 lineExact file
Filter.Tendsto (fun n => ↑(Erdos624.H n) - Real.logb 2 ↑n) Filter.atTop Filter.atTop
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page