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 ℘.
!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;
br
txt \(x \mapsto \{x\}\) は \(X\) から \(\wp X\) への単射になる。
thm `X ≤# ℘ X` ◀ W. , ax_s
prf |g_ := `\{ \< pr x ; \{ set x \} \> Cls x | x ∈ |X \}` ;
    hyG <- `|g =_ |g_` ;
    Leg <- `|g_ ⊂_ |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];

section 証明①
forget{
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];
forget}

section 証明②
forget{
word ^sw
prop ^sw. <- `R ^sw =_ \{ \< pr y ; x \> Cls x ; y | \< pr x ; y \> ∈ R \}`
prop/thm →IS^sw <- `f ∈ X →IS Y ⟹ f ^sw ∈ Y →IS X` ◀ W.
prf →IS^sw //// W.'!=. -| pr:0 p; →IS^sw -| W. h;
br
txt 単射 \(g : \wp X \to X\) に対して \(B = \{g(A) \mid A \subset X , g(A) \notin A\}\) とすると \(B \in \wp X\)。
txt \(g(B) \in B\) なら \(g(B) = g(A)\)、\(g(A) \notin A\) となる \(A\) があり、単射だから \(A = B\) で \(g(B) \notin B\)。
txt \(g(B) \notin B\) なら \(A = B\) として \(g(B) \in B\)。どちらも矛盾する。
thm `℘ X {/}≤# X` ◀ W. , ax_s
prf B_ := `\{ cls x ∈ |X | ∃ A \, (\< pr A ; x \> ∈ |g and x {/}∈ A) \}` ;
    hyB <- `|B =_ B_` ;
    LBs <- `B_ ⊂_ |X` -| O p;
    LBp <- `|B ∈ ℘ |X` / W.' -| hyB p;
    LeB <- `|g {/}∈ ℘ |X →I |X` / →I. / W.' -| LBp , hyB , pr:0 p;
    Lgen <- `g {/}∈ ℘ X →I X` -| W. , ax_s h[fix];
    goal / ≤#.' -| Lgen p;
    goal -| W. , ax_s h;
br
txt 全単射 \(f : X \to \wp X\) があれば逆 \(f^{-1}\) は \(\wp X\) から \(X\) への全単射になるので、2つの結果を合わせると \(\wp X\) は \(X\) より真に大きい。
thm `X <# ℘ X` ◀ W. , ax_s
prf goal / <#. / =#.' -| `X ≤# ℘ X` , `℘ X {/}≤# X` / ≤#.' , →IS^sw , →IS. p;
    goal -| W. , ax_s h;
forget}

articles1/63.book

`articles1/63.book`