Wetzel's Problem and the Continuum Hypothesis

Title:	Wetzel's Problem and the Continuum Hypothesis
Author:	Lawrence C Paulson
Submission date:	2022-02-18
Abstract:	Let $F$ be a set of analytic functions on the complex plane such that, for each $z\in\mathbb{C}$, the set $\{f(z) \mid f\in F\}$ is countable; must then $F$ itself be countable? The answer is yes if the Continuum Hypothesis is false, i.e., if the cardinality of $\mathbb{R}$ exceeds $\aleph_1$. But if CH is true then such an $F$, of cardinality $\aleph_1$, can be constructed by transfinite recursion. The formal proof illustrates reasoning about complex analysis (analytic and homomorphic functions) and set theory (transfinite cardinalities) in a single setting. The mathematical text comes from Proofs from THE BOOK by Aigner and Ziegler.
BibTeX:	@article{Wetzels_Problem-AFP, author = {Lawrence C Paulson}, title = {Wetzel's Problem and the Continuum Hypothesis}, journal = {Archive of Formal Proofs}, month = feb, year = 2022, note = {\url{https://isa-afp.org/entries/Wetzels_Problem.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	ZFC_in_HOL
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.