Formal target: Corpus.Erdos624.erdos_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$.
Exact formal statement
Filter.Tendsto.{0, 0} (fun n => HSub.hSub.{0, 0, 0} (Nat.cast.{0} (Corpus.Erdos624.H n)) (Real.logb 2 (Nat.cast.{0} n)))
Filter.atTop.{0} Filter.atTop.{0}This target is a formal statement, not a proof of the problem.
Environment availability: available.