book集

txt 52a は自然数 \(n\)（集合 \(\{0, \dots, n-1\}\)）の部分集合を数えた。ここでは \(n\) と対等な任意の集合 \(X\) に広げる。
section 対等な集合のべき集合
word* *^ap
prop *^ap.
txt \(f[A]\) は \(A\) の \(f\) による像。像が集合であることは *^ap. の定義が仮定として含む（置換公理に当たる）。
txt 全単射 \(f : X \to Y\) は \(A \mapsto f[A]\) で \(\wp X\) から \(\wp Y\) への全単射を与える。
let/thm ℘=# <- `X =# Y ⟹ ℘ X =# ℘ Y` ◀ W. , ax_s
prf hyf <- `|f ∈ |X →IS |Y` ;
    hf0 <- `\< pr x ; y \> ∈ |f ⟹ x ∈ |X and y ∈ |Y` -| hyf /// W.'!=. , pr:0 p;
    hfF <- `\< pr x ; y \> ∈ |f and \< pr x ; z \> ∈ |f ⟹ y = z` -| hyf /// W.'!=. , hf0 , pr:0 p;
    hfU <- `\< pr x ; y \> ∈ |f and \< pr z ; y \> ∈ |f ⟹ x = z` -| hyf /// W.'!=. , hf0 , pr:0 p;
    hfX <- `x ∈ |X ⟹ [ ∃ y \, \< pr x ; y \> ∈ |f ]` -| hyf /// W.'!=. , pr:0 p;
    hfY <- `y ∈ |Y ⟹ [ ∃ x \, \< pr x ; y \> ∈ |f ]` -| hyf /// W.'!=. , pr:0 p;
    Im1 <- `|f *^ap (A) ⊂ |Y` / ⊂. / *^ap. -| hf0 p;
    Inj <- `A ⊂ |X and C ⊂ |X and |f *^ap (A) = |f *^ap (C) ⟹ A = C` / =. / ⊂. / *^ap. -| hfX , hfU p;
    Sur1 <- `|f ^sw *^ap (B) ⊂ |X` / ⊂. / *^ap. / ^sw. -| hf0 , pr:0 p;
    Sur2 <- `B ⊂ |Y ⟹ |f *^ap (|f ^sw *^ap (B)) = B` / =. / ⊂. // *^ap. / ^sw. -| hfF , hfY , pr:0 p;
    |F_ := `\{ \< pr A ; |f *^ap (A) \> Cls A | A ∈ ℘ |X \}` ;
    hyF <- `|F =_ |F_` ;
    LFm <- `\< pr A ; B \> ∈ |F ⟺ A ⊂ |X and B = |f *^ap (A)` -| hyF / W.!=. , pr:0 p;
    LFz <- `z ∈ |F ⟹ [ ∃ A \, A ⊂ |X and z = \< pr A ; |f *^ap (A) \> ]` -| hyF / W.!=. p;
    LFs <- `|F_ ⊂_ ℘ |X ^^pr ℘ |Y` /// W.'!=. -| Im1 / ⊂. p;
    LF0 <- `|F ⊂ ℘ |X ^^pr ℘ |Y` / ⊂. / ^^pr. -| LFz , Im1 , ℘.' , ⊂. p;
    LF1 <- `[ ∀ A ∈ ℘ |X . [ ∃！ B \, \< pr A ; B \> ∈ |F ] ]` -| LFm , ℘.' , ⊂. p;
    LF2 <- `[ ∀ B ∈ ℘ |Y . [ ∃！ A \, \< pr A ; B \> ∈ |F ] ]` -| LFm , ℘.' , ⊂. , Inj , Sur1 , Sur2 p;
    LFi <- `|F ∈ ℘ |X →IS ℘ |Y` / →IS. -| LF0 , LF1 , LF2 p;
    `℘ |X =# ℘ |Y` / =#.' -| LFi p;
    Lf <- `f ∈ X →IS Y ⟹ ℘ X =# ℘ Y` -| W. , ax_s h[fix];
    ℘=# / =#.' -| Lf / =#.' p;
    ℘=# -| W. , ax_s h;
section 主定理
txt よって \(n\) 個の元をもつ集合の部分集合は \(2^n\) 個（52a の主定理と ℘=#）。
thm `n ∈ 𝕄 and X =# n ⟹ ℘ X =# 2 ↑ n` ◀ W. , ax_s , +𝕄 , *𝕄 , ↑𝕄
prf goal -| ℘=# , `n ∈ 𝕄 ⟹ ℘ n =# 2 ↑ n` , =#:T p;
    goal -| W. , ax_s , +𝕄 , *𝕄 , ↑𝕄 h;

articles2/52b.book

`articles2/52b.book`