book集

txt 52a・52b・58 などで共通に使う準備：集合の基本・全単射と個数（=#）・集合で作る自然数と帰納法・加法と個数。
section 準備
subsection andの縦表記
abbr And

subsection 基本的な集合関数
word ∅
prop ∅.
!prop/thm ∅.' ◀ W.
prf ∅.' // W. -| O p; ∅.' -| W. h;
br
word set\n
abbr set
prop set\n.
br
word ∪ ∩
prop ∪. <- `X ∪ Y =_ \{ cls x | x ∈ X or x ∈ Y \}`
prop ∩. <- `X ∩ Y =_ \{ cls x | x ∈ X and x ∈ Y \}`
br
word ℘
prop ℘.
!prop/thm ℘.' ◀ W.
prf ℘.' -| W. p;

subsection 順序対、直積
word \pr
abbr pr
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 \}`
word ^sw
prop ^sw. <- `R ^sw =_ \{ \< pr y ; x \> Cls x ; y | \< pr x ; y \> ∈ R \}`
word ∘
prop ∘.

subsection 全単射
word →IS
prop →IS. <- `X →IS Y =_ \{ cls f ⊂ X ^^pr Y | [ ∀ x ∈ X . [ ∃！ y \, \< pr x ; y \> ∈ f ] ] and [ ∀ y ∈ Y . [ ∃！ x \, \< pr x ; y \> ∈ f ] ] \}`
prop/thm →IS^sw ◀ W.
prf →IS^sw /// W.'!=. -| pr:0 p; →IS^sw -| W. h;
prop/thm →IS∘ ◀ W.
prf →IS∘ /// W.'!=. -| pr:0 p; →IS∘ -| W. h;
prop/thm →IS∪ <- `\\{ And f ∈ X →IS X' \\ g ∈ Y →IS Y' \\} and \\{ And X ∩ Y = ∅ \\ X' ∩ Y' = ∅ \\} ⟹ f ∪ g ∈ X ∪ Y →IS X' ∪ Y'` ◀ W.
prf →IS∪ //// W.'!=. -| pr:0 v; →IS∪ -| W. h;
br
word id
prop id. <- `id _ X =_ \{ \< pr x ; x \> Cls x | x ∈ X \}`
prop/thm id:0 ◀ W.
prf id:0 /// W.'!=. -| pr:0 p; id:0 -| W. h;
br
word =#
prop =#.
!prop/thm =#.' ◀ W.
prf =#.' / =#. / ∅.' -| O p; =#.' -| W. h;
prop/thm =#:R <- `X =# X` ◀ W.
prf =#:R / =#.' / W. -| id:0 / W. p; =#:R -| W. h;
prop/thm =#:T <- `[ chain X =# Y =# Z ] ⟹ X =# Z` ◀ W.
prf =#:T / =#.' -| →IS∘ p; =#:T -| W. h;
prop/thm =#:X ◀ W.
prf =#:X / =#.' -| →IS^sw p; =#:X -| W. h;
prop/thm =#∪ <- `\\{ And X =# X' \\ Y =# Y' \\} and \\{ And X ∩ Y = ∅ \\ X' ∩ Y' = ∅ \\} ⟹ X ∪ Y =# X' ∪ Y'` ◀ W.
prf =#∪ / =#.' -| →IS∪ p; =#∪ -| W. h;

newpage
section 自然数

subsection 0と後続関数
word 0
prop 0.
!prop/thm 0.' ◀ W.
prf 0.' / W. -| O p; 0.' -| W. h;
word suc ^suc
prop suc.
!prop/thm suc.' ◀ W.
prf suc.' // W.!=. -| O p; suc.' -| W. h;
prop ^suc. <- `X ^suc =_ \{ x suc Cls x | x ∈ X \}`

subsection 帰納法
word ⋂_
prop ⋂_.
word Ind
prop Ind.
word 𝕄
prop 𝕄.
txt 𝕄 は集合の語なので、𝕄. は \(\bigcap {\rm Ind}\) が集合であること＝無限公理に当たる内容を含みます。
!prop/thm 𝕄1 ◀ W.
prf 𝕄1 /// W.'!=. -| O p; 𝕄1 -| W. h;
!thm `0 ∈ 𝕄` ◀ W.
prf goal / 𝕄. -| O p; goal -| W. h;
thm `𝕄 ∈_ Ind` ◀ W.
prf goal -| `0 ∈ 𝕄` , 𝕄1 , ⊂. , ^suc. p; goal -| W. h;
!prop/thm INDC <- `0 ∈_ D_ and [ ∀ m ∈ 𝕄 . (m ∈_ D_ ⟹ m suc ∈_ D_) ] and n ∈ 𝕄 ⟹ n ∈_ D_` ◀ W. , ax_s
prf B_ := `\{ cls x ∈ 𝕄 | x ∈_ D_ \}` ;
    LI <- `0 ∈ B and [ ∀ m ∈ 𝕄 . (m ∈ B ⟹ m suc ∈ B) ] ⟹ 𝕄 ∩ B ∈_ Ind and 𝕄 ∩ B ⊂_ B` / ⊂. / ^suc. / ∩. -| `0 ∈ 𝕄` , 𝕄1 p;
    INDS <- `0 ∈ B and [ ∀ m ∈ 𝕄 . (m ∈ B ⟹ m suc ∈ B) ] and n ∈ 𝕄 ⟹ n ∈ B` / 𝕄. -| LI / 𝕄. p;
    INDC --| INDS , ax_s[C_:=`B_`] , `0 ∈ 𝕄` , 𝕄1 v;
    INDC -| W. , ax_s h[lift];
let/thm Lirr <- `n ∈ 𝕄 ⟹ n {/}∈ n` ◀ W. , ax_s
prf Lirr -| INDC[D_:=`\{ cls n | [ ∀ m ∈ n . m ⊂ n and m {/}= n ] \}`] / ⊂. / 0.' , suc.' v; Lirr -| W. , ax_s h;
!let/thm Lpred <- `k ∈ 𝕄 and k {/}= 0 ⟹ [ ∃ j ∈ 𝕄 . k = j suc ]` ◀ W. , ax_s
prf Lpred -| INDC[D_:=`\{ cls k | k = 0 or [ ∃ j ∈ 𝕄 . k = j suc ] \}`] , 𝕄1 p; Lpred -| W. , ax_s h;

subsection 自然数の演算
word +
prop +𝕄
let/thm +∈𝕄 <- `[ m ; n col ∈ 𝕄 ] ⟹ m + n ∈ 𝕄` ◀ W. , ax_s , +𝕄
prf +∈𝕄 -| INDC[D_:=`\{ cls n | m + n ∈ 𝕄 \}`] , +𝕄 , 𝕄1 p;
    +∈𝕄 -| W. , ax_s , +𝕄 h;
let/thm +1 <- `m ∈ 𝕄 ⟹ m suc = m + 1` ◀ W. , +𝕄
prf L1 <- `1 = 0 suc` / W. /// W.!=. -| O p; +1 -| +𝕄 , L1 , `0 ∈ 𝕄` p; +1 -| W. , +𝕄 h;
!let/thm L×0 <- `\{ set c \} ^^pr m =# m` ◀ W. , ax_s
prf |K_ := `\{ \< pr \< pr |c ; x \> ; x \> Cls x | x ∈ |m \}` ;
    hyK <- `|K =_ |K_` ;
    LKs <- `|K_ ⊂_ (\{ set |c \} ^^pr |m) ^^pr |m` /// W.!=. -| O p;
    LKi <- `|K ∈ (\{ set |c \} ^^pr |m) →IS |m` ///// W.!=. -| hyK ///// W.!=. , pr:0 p;
    `\{ set |c \} ^^pr |m =# |m` / =#.' -| LKi p;
    L×0 -| W. , ax_s h[fix];
txt 1点を足すと個数は1つ増える（Ladd）。\(n \notin B\) なら \(B \mapsto B \cup \{n\}\) は単射で、\(n\) を含む \(n+1\) の部分集合はこの形（LJ2・LB）。
!let/thm Ladd <- `B =# j and n {/}∈ B and j ∈ 𝕄 ⟹ B ∪ \{ set n \} =# j + 1` ◀ W. , ax_s , +𝕄
prf L11a <- `\{ set \< pr a ; b \> \} ∈ \{ set a \} →IS \{ set b \}` //// W.'!=. -| pr:0 p;
    L11 <- `\{ set a \} =# \{ set b \}` / =#.' -| L11a p;
    Ld1 <- `a {/}∈ Y ⟹ Y ∩ \{ set a \} = ∅` / =. /// W.'!=. -| O p;
    Ladd -| =#∪ , L11 , Ld1 , Lirr , suc. , +1 v;
    Ladd -| W. , ax_s , +𝕄 h;
!let/thm LJ2 <- `n {/}∈ A and n {/}∈ C and A ∪ \{ set n \} = C ∪ \{ set n \} ⟹ A = C` ◀ W.
prf LJ2 /// W. -| O p; LJ2 -| W. h;
!let/thm LB <- `B ⊂ n suc and n ∈ B ⟹ B ∩ n ⊂ n and B = (B ∩ n) ∪ \{ set n \}` ◀ W.
prf LB /// W. -| O p; LB -| W. h;
txt \(m + n\) は、\(m\) 個と \(n\) 個を印 \(c \neq d\) で区別して並べた集合 \(\{c\} \times m \cup \{d\} \times n\) の個数。
let/thm +=#g <- `c {/}= d and [ m ; n col ∈ 𝕄 ] ⟹ m + n =# \{ set c \} ^^pr m ∪ \{ set d \} ^^pr n` ◀ W. , ax_s , +𝕄
prf LDsuc <- `\{ set c \} ^^pr m ∪ \{ set d \} ^^pr n suc = (\{ set c \} ^^pr m ∪ \{ set d \} ^^pr n) ∪ \{ set \< pr d ; n \> \}` / =. //// W.'!=. -| O p;
    Lu <- `\{ set c \} ^^pr m ∪ \{ set d \} ^^pr 0 = \{ set c \} ^^pr m` / =. /// W.'!=. -| O p;
    Ln <- `c {/}= d and n ∈ 𝕄 ⟹ \< pr d ; n \> {/}∈ \{ set c \} ^^pr m ∪ \{ set d \} ^^pr n` / ∪. / ^^pr. / set1. -| pr:0 , Lirr p;
    L+s <- `c {/}= d and [ m ; n col ∈ 𝕄 ] and \{ set c \} ^^pr m ∪ \{ set d \} ^^pr n =# m + n ⟹ \{ set c \} ^^pr m ∪ \{ set d \} ^^pr n suc =# m + n suc` -| LDsuc , Ln , Ladd , +∈𝕄 , +𝕄 , +1 v;
    +=#g -| INDC[D_:=`\{ cls n | \{ set c \} ^^pr m ∪ \{ set d \} ^^pr n =# m + n \}`] , L×0 , +𝕄 , Lu , L+s , =#:X p;
    +=#g -| W. , ax_s , +𝕄 h;
br
txt 交わらない \(m\) 個と \(k\) 個を合わせると \(m + k\) 個。
let/thm ∪=#+ <- `X ∩ Y = ∅ and [ m ; k col ∈ 𝕄 ] and X =# m and Y =# k ⟹ X ∪ Y =# m + k` ◀ W. , ax_s , +𝕄
prf L01 <- `0 {/}= 1` // W. -| O p;
    LD <- `\{ set 0 \} ^^pr m ∩ \{ set 1 \} ^^pr k = ∅` / =. /// W.'!=. -| pr:0 , L01 p;
    ∪=#+ -| =#∪ , +=#g , L×0 , =#:T , =#:X , L01 , LD v;
    ∪=#+ -| W. , ax_s , +𝕄 h;

articles2/0-sn.book

`articles2/0-sn.book`