集合論

目次 集合論で出てくる濃度という概念が非常に謎だったので調べてみました。 濃度とは 集合論における濃度（cardinality） は、集合の「大きさ」や「要素の個数」を表す概念です。有限集合なら「要素の個数」と同じですが、無限集合にも拡張された抽象的な「大きさ」の指標です。 1. 直観的なイメージ 有限集合：「集合 A の濃度」は、A に含まれる要素の個数です。例：A = {1, 2, 3} なら |A| = 3。 無限集合：自然数全体の集合 ℕ と、整数全体の集合 ℤ はどちらも無限個の要素を持ちますが、「同じ種類の無限」かどうかを比較するために濃度を使います。 2. 濃度の厳密な定義（同値…

はじめに こんにちはiimonでフロントエンドエンジニアをしている「みよちゃん」です！ 普段業務でTypeScriptを使用していますが、皆さんもご存じのSetに関して、重複を削除する以外の用途で使用したことがなく、いまいちピンときていませんでした。 最近個人的に数学を勉強する機会があり、その中の一つに「群論」がありました。これは、代数学の基礎になる分野で「集合」や「関係」を含みます。この集合・関係について学ぶなかで、Setについてハッと思う部分があったので、まとめたいと思います！ ※この記事はお堅いタイトルですが、自分が数学を勉強する中でふと思ったことをベースに書いているため、数学的理論に基…

第4章「集合と関数」の最後のセクションはシュレーダー＝ベルンシュタインの定理のLean4による証明です。 初めてこの定理をきちんとした形で知りました。集合論の濃度に関する基本的な定理です。 定理：$\alpha, \beta$を集合、$f:\alpha \rightarrow\beta, g:\beta\rightarrow\alpha$が両方とも単射である時、$\alpha$から$\beta$への全単射がある。 集合の濃度に関して$|\alpha| \ge |\beta|, |\beta|\ge|\alpha|$のとき$|\alpha|=|\beta|$が成り立つということで確かに基本的です…

Mathematics in LeanもC04 Sets and Functionsの最初の章である集合まで辿り着きました。ここでは集合に関する性質の証明方法のLean4での実現の仕方を知ります。 集合が等しいこと(A=B)を示す場合、ゴールをA=Bとして方法として、AがBの部分集合であり、かつBがAの部分集合であることを示すこと AがBの部分集合であることを示すにはAの任意の要素がBの要素であることを示すこと 空集合と全体集合の性質 和集合と積集合をメンバーシップの論理和と論理積 集合族の積集合と和集合 のようなことがここでは解説されています。ここでは上記の初めの２つについて簡単な命題を示し…