### 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.

### License

BSD License

### Topics

- Mathematics/Analysis
- Logic/Set theory

### Session Wetzels_Problem

- Wetzels_Problem

### Depends on

- Zermelo Fraenkel Set Theory in Higher-Order Logic

### Auto-related entries

- Euler’s Polyhedron Formula
- Lucas’s Theorem
- Evaluate Winding Numbers through Cauchy Indices
- The number of comparisons in QuickSort
- The Cartan Fixed Point Theorems

## Cite

×

Wetzels_Problem-AFP

    @article{Wetzels_Problem-AFP,
      author  = {Lawrence C. Paulson},
      title   = {Wetzel's Problem and the Continuum Hypothesis},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Wetzels_Problem.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Feb 21, 2022 : Isabelle2021-1