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's theorem [Er64g], answering a question of Wetzel: if , then every family of entire functions taking only countably many distinct values at each point is itself countable.
Cardinal.aleph 1 < Cardinal.continuum → ∀ (F : Set (ℂ → ℂ)), (∀ f ∈ F, Differentiable ℂ f) → (∀ (z₀ : ℂ), {y | ∃ f ∈ F, f z₀ = y}.Countable) → F.CountableSolvedStatement only, no proof