book集

section 準備

subsection 空集合、有限集合、べき集合
word ∅
prop ∅.
prop/thm ∅.' ◀ W.
prf ∅.' // W. -| O p; ∅.' -| W. h;
br
word set\n
abbr set
prop set\n.
br
word ℘
prop ℘.
txt ℘ は集合の語なので、℘. は \(\{A \mid A \subset X\}\) が集合であること＝冪集合公理を含みます。
!prop/thm ℘.' ◀ W.
prf ℘.' -| W. p;

subsection 順序対、直積
word \pr
abbr pr
br
word ◁ ▷
prop ◁.
prop ▷.
prop/thm pr:0 ◀ W.
prf pr:0 -| ◁. , ▷. p;
    pr:0 -| W. h;
br
word ^^pr
prop ^^pr. <- `X ^^pr Y =_ \{ \< pr x ; y \> Cls x ; y | x ∈ X and y ∈ Y \}`

subsection 写像、集合の大きさ比較
txt \(X \to Y\) は \(X\) から \(Y\) への写像全体の集合。矢印の上の I・S・IS は単射・全射・全単射を表す。
word → →I →S →IS
prop →. <- `X → Y =_ \{ cls f ⊂ X ^^pr Y | [ ∀ x ∈ X . [ ∃！ y \, \< pr x ; y \> ∈ f ] ] \}`
!prop/thm →.' ◀ W.
prf →.' /// W.!=. -| O p; →.' -| W. h;
prop →I. <- `X →I Y =_ \{ cls f ∈ X → Y | ∀ y \, [ ！ x \, \< pr x ; y \> ∈ f ] \}`
prop →S. <- `X →S Y =_ \{ cls f ∈ X → Y | [ ∀ y ∈ Y . [ ∃ x \, \< pr x ; y \> ∈ f ] ] \}`
prop →IS. <- `X →IS Y =_ \{ cls f | f ∈ X →I Y and f ∈ X →S Y \}`
br
word =# ≤# <#
prop =#.
prop ≤#.
prop <#.
!prop/thm =#.' ◀ W.
prf =#.' / =#. / ∅.' -| O p; =#.' -| W. h;
!prop/thm ≤#.' ◀ W.
prf ≤#.' / ≤#. / ∅.' -| O p; ≤#.' -| W. h;

section 主定理
txt \(x \mapsto \{x\}\) は \(X\) から \(\wp X\) への単射になる。
thm `X ≤# ℘ X` ◀ W. , ax_s
prf α_ := `\{ \< pr x ; \{ set x \} \> Cls x | x ∈ |X \}` ;
    hyG <- `|g =_ α_` ;
    Leα <- `α_ ⊂_ |X ^^pr ℘ |X` // W.'!=. -| set1. p;
    LeI <- `|g ∈ |X →I ℘ |X` /// W.'!=. -| hyG /// W.'!=. , pr:0 , set1. p;
    `|X ≤# ℘ |X` / ≤#.' -| LeI p;
    goal -| W. , ax_s h[fix];
br
txt 写像 \(f : X \to \wp X\) に対して \(A = \{x \in X \mid x \notin f(x)\}\) とすると \(A \in \wp X\)。
txt \(A = f(a)\) となる \(a \in X\) があれば \(a \in A \iff a \notin A\) となって矛盾する（対角線論法）。
txt よって \(f\) は全射でなく、特に全単射は無い。
thm `X {/}=# ℘ X` ◀ W. , ax_s
prf A_ := `\{ cls x ∈ |X | {/}∃ y \, (\< pr x ; y \> ∈ |f and x ∈ y) \}` ;
    hyA <- `|A =_ A_` ;
    LAs <- `A_ ⊂_ |X` -| O p;
    LeA <- `|f ∈ |X → ℘ |X ⟹ |f {/}∈ |X →S ℘ |X` / →S. / W.' -| hyA , pr:0 v;
    Lgen <- `f ∈ X → ℘ X ⟹ f {/}∈ X →S ℘ X` -| W. , ax_s h[fix];
    goal / =#.' / →IS. / →I. -| Lgen p;
    goal -| W. , ax_s h;
br
txt 2つの結果を合わせると、\(\wp X\) は \(X\) より真に大きい。
thm `X <# ℘ X` ◀ W. , ax_s
prf `|X <# ℘ |X` / <#. -| `X ≤# ℘ X` , `X {/}=# ℘ X` p;
    goal -| W. , ax_s h[fix];

articles1/63.book

`articles1/63.book`