Proposition I.5.7 (実数の非可算性)
- Proposition I.5.7 (実数の非可算性) #Card
- $\mathbb{R}$ は非可算。本書の（対角線論法によらない）証明の方針は？
The set $\mathbb{R}$ of real numbers is uncountable. $\operatorname{card} \mathbb{R}$ is denoted $\mathfrak{c}$ and called the continuum.
本書の証明（入れ子区間式）: 全射 $\varphi \in \mathbb{R}^\mathbb{N}$ があったとして、$\varphi(n_{2k}) < \varphi(n_{2k+2}) < \dots < \varphi(n_{2k+3}) < \varphi(n_{2k+1})$ となる狭義増加添字列を構成。$\mathbb{R}$ の相対完備性（cards/topology/extended-real-line）より $$\sup_k \varphi(n_{2k}) \leq r \leq \inf_k \varphi(n_{2k+1})$$ なる $r$ が存在し、構成より $r \notin \varphi(\mathbb{N})$——矛盾。
- 完備性（sup の存在）が本質という点で、Cantor の対角線論法（cards/topology/thm-i-5-8-cantor）と相補的。
Cardinal.not_countable_real
本ノート RoyalRoad.ChapterI.prop_I_5_7_real_uncountable（Notes/ChapterI.lean、lake build 済み）