Erdős problem 1119
Let be an infinite cardinal with . Let be a family of entire functions such that, for every , there are at most distinct values of . Must have cardinality at most ?
Sources
FormalConjectures/ErdosProblems/
1119.lean
Retained formal statement
Erdős [Er64g] also showed that the previous statement fails under the continuum hypothesis: if , then there is an uncountable family of entire functions taking only countably many distinct values at each point .
Cardinal.continuum = Cardinal.aleph 1 → ∃ F, (∀ f ∈ F, Differentiable ℂ f) ∧ (∀ (z₀ : ℂ), {y | ∃ f ∈ F, f z₀ = y}.Countable) ∧ ¬F.CountableSolvedStatement only, no proof