Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Wetzel's Problem and the Conti...


view this post on Zulip Email Gateway (Feb 21 2022 at 16:58):

From: Tobias Nipkow <nipkow@in.tum.de>
Wetzel's Problem and the Continuum Hypothesis
Lawrence C Paulson

Let F be a set of analytic functions on the complex plane such that, for each z
: C, the set {f(z) | f : 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
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.

https://www.isa-afp.org/entries/Wetzels_Problem.html

Enjoy!
smime.p7s


Last updated: Jul 15 2022 at 23:21 UTC