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
Sanity check: the empty family of entire functions satisfies both the value-bound hypothesis and the cardinality conclusion of erdos_1119, for any infinite .
∀ (m : Cardinal.{0}), Cardinal.aleph0 < m → (∀ f ∈ ∅, Differentiable ℂ f) ∧ (∀ (z₀ : ℂ), Cardinal.mk ↑{y | ∃ f ∈ ∅, f z₀ = y} ≤ m) ∧ Cardinal.mk ↑∅ ≤ mTestStatement only, no proof