book集

section 2の冪と奇数
txt \(2^a(2b+1)\) の形の表し方は1通り（Linj）。
let/thm Linj <- `[ a ; b ; c ; d col ∈ 𝕄 ] and 2 ↑ a ⋅ (2 ⋅ b + 1) = 2 ↑ c ⋅ (2 ⋅ d + 1) ⟹ a = c and b = d` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1. , 2.
prf Lo <- `b ∈ 𝕄 ⟹ 2 ⋅ b + 1 ∈ 𝕄` -| ⋅∈𝕄 , +∈𝕄 , `2 ∈ 𝕄` , 𝕄0s , 1. p;
    E0 <- `y ∈ 𝕄 ⟹ 2 ↑ 0 ⋅ y = y` -| ↑𝕄 , ⋅C , L⋅1 , `2 ∈ 𝕄` , 𝕄0s , 1. p;
    Es <- `[ x ; y col ∈ 𝕄 ] ⟹ 2 ↑ { x suc } ⋅ y = 2 ⋅ (2 ↑ x ⋅ y)` -| ↑𝕄 , ⋅A , ⋅C , ↑∈𝕄 , `2 ∈ 𝕄` v;
    Lb <- `[ ∀ b ∈ 𝕄 . [ ∀ c ∈ 𝕄 . [ ∀ d ∈ 𝕄 . (2 ↑ 0 ⋅ (2 ⋅ b + 1) = 2 ↑ c ⋅ (2 ⋅ d + 1) ⟹ 0 = c and b = d) ] ] ]` -| Lpred , E0 , Es , Lne , L1K , Lo , ↑∈𝕄 , ⋅∈𝕄 , `2 ∈ 𝕄` v;
    S0 <- `[ a ; b ; d col ∈ 𝕄 ] ⟹ 2 ↑ { a suc } ⋅ (2 ⋅ b + 1) {/}= 2 ↑ 0 ⋅ (2 ⋅ d + 1)` -| Es , E0 , Lne , Lo , ↑∈𝕄 , ⋅∈𝕄 , `2 ∈ 𝕄` v;
    S1 <- `[ a ; b ; j ; d col ∈ 𝕄 ] and 2 ↑ { a suc } ⋅ (2 ⋅ b + 1) = 2 ↑ { j suc } ⋅ (2 ⋅ d + 1) ⟹ 2 ↑ a ⋅ (2 ⋅ b + 1) = 2 ↑ j ⋅ (2 ⋅ d + 1)` -| Es , L2K , Lo , ↑∈𝕄 , ⋅∈𝕄 , `2 ∈ 𝕄` v;
    Ls <- `a ∈ 𝕄 and [ ∀ b ∈ 𝕄 . [ ∀ c ∈ 𝕄 . [ ∀ d ∈ 𝕄 . (2 ↑ a ⋅ (2 ⋅ b + 1) = 2 ↑ c ⋅ (2 ⋅ d + 1) ⟹ a = c and b = d) ] ] ] ⟹ [ ∀ b ∈ 𝕄 . [ ∀ c ∈ 𝕄 . [ ∀ d ∈ 𝕄 . (2 ↑ { a suc } ⋅ (2 ⋅ b + 1) = 2 ↑ c ⋅ (2 ⋅ d + 1) ⟹ a suc = c and b = d) ] ] ]` -| Lpred , S0 , S1 , 𝕄0s v;
    Linj -| IND𝕄[C_:=`\{ cls a | [ ∀ b ∈ 𝕄 . [ ∀ c ∈ 𝕄 . [ ∀ d ∈ 𝕄 . (2 ↑ a ⋅ (2 ⋅ b + 1) = 2 ↑ c ⋅ (2 ⋅ d + 1) ⟹ a = c and b = d) ] ] ] \}`] , Lb , Ls v;
    Linj -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1. , 2. h;

newpage
section 有理数
subsection 順序対・写像
word \pr
abbr pr
word ◁ ▷
prop ◁.
prop ▷.
prop/thm pr:0 ◀ W.
prf pr:0 -| ◁. , ▷. p; pr:0 -| W. h;
word ^^pr
prop ^^pr. <- `X ^^pr Y =_ \{ \< pr x ; y \> Cls x ; y | x ∈ X and y ∈ Y \}`
txt \(X \to Y\) は \(X\) から \(Y\) への写像全体の集合、\(X \overset{S}{\to} Y\) は全射全体の集合。
word → →S
prop →. <- `X → Y =_ \{ cls f ⊂ X ^^pr Y | [ ∀ x ∈ X . [ ∃！ y \, \< pr x ; y \> ∈ f ] ] \}`
prop →S. <- `X →S Y =_ \{ cls f ∈ X → Y | [ ∀ y ∈ Y . [ ∃ x \, \< pr x ; y \> ∈ f ] ] \}`

subsection 整数と有理数
txt 整数は自然数 \(n\) と \(-n\)、有理数は分数 \(a \div b\)（\(a\) は整数、\(b\) は 0 でない自然数）。
txt 可算性には \(-\) と \(\div\) の性質（\(-0 = 0\) や約分など）は要らないので、何も仮定しません。
word -
word ÷
word ℤ ℚ
prop ℤ. <- `ℤ =_ \{ cls a | a ∈ 𝕄 or [ ∃ n ∈ 𝕄 . a = - n ] \}`
prop ℚ. <- `ℚ =_ \{ a ÷ b Cls a ; b | a ∈ ℤ and b ∈ 𝕄 and b {/}= 0 \}`

newpage
section 主定理
txt 自然数 \(k\) を \(2^m(2n+1)\) と表し（表し方は1通り＝Linj）、\(m\) の偶奇で整数の符号を決めて、\(k\) に有理数 \(\pm i \div (n+1)\)（\(m = 2i\) なら \(+\)、\(m = 2i+1\) なら \(-\)）を対応させる。\(k = 0\) は \(0 \div 1\) に送る。
txt どの有理数 \(a \div b\) も、\(b = n+1\)、\(a = i\) なら \(m = 2i\)、\(a = -i\) なら \(m = 2i+1\) として値に現れるので、この対応は全射。
thm `[ ∃ f \, f ∈ 𝕄 →S ℚ ]` ◀ W. , ax_s , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄
prf f_ := `\{ \< pr k ; q \> Cls k ; q | k ∈ 𝕄 and ([ ∃ m ∈ 𝕄 . [ ∃ n ∈ 𝕄 . [ ∃ i ∈ 𝕄 . k = 2 ↑ m ⋅ (2 ⋅ n + 1) and ((m = 2 ⋅ i and q = i ÷ (n suc)) or (m = 2 ⋅ i + 1 and q = (- i) ÷ (n suc))) ] ] ] or (¬ [ ∃ m ∈ 𝕄 . [ ∃ n ∈ 𝕄 . k = 2 ↑ m ⋅ (2 ⋅ n + 1) ] ] and q = 0 ÷ (0 suc))) \}` ;
    hyF <- `|f =_ f_` ;
    Lsub <- `f_ ⊂_ 𝕄 ^^pr ℚ` //// W.!=. -| suc𝕄 , 𝕄0s v;
    Lmem <- `\< pr k ; q \> ∈ |f ⟹ k ∈ 𝕄 and ([ ∃ m ∈ 𝕄 . [ ∃ n ∈ 𝕄 . [ ∃ i ∈ 𝕄 . k = 2 ↑ m ⋅ (2 ⋅ n + 1) and ((m = 2 ⋅ i and q = i ÷ (n suc)) or (m = 2 ⋅ i + 1 and q = (- i) ÷ (n suc))) ] ] ] or (¬ [ ∃ m ∈ 𝕄 . [ ∃ n ∈ 𝕄 . k = 2 ↑ m ⋅ (2 ⋅ n + 1) ] ] and q = 0 ÷ (0 suc)))` -| hyF , pr:0 v;
    LV <- `[ m ; i ; j col ∈ 𝕄 ] and ((m = 2 ⋅ i and q = i ÷ (n suc)) or (m = 2 ⋅ i + 1 and q = (- i) ÷ (n suc))) and ((m = 2 ⋅ j and r = j ÷ (n suc)) or (m = 2 ⋅ j + 1 and r = (- j) ÷ (n suc))) ⟹ q = r` -| L2K , L1K , Lne v;
    Luni <- `\< pr k ; q \> ∈ |f and \< pr k ; r \> ∈ |f ⟹ q = r` -| Lmem , Linj , LV v;
    Lfto <- `k ∈ 𝕄 ⟹ [ ∃ q \, \< pr k ; q \> ∈ |f ]` -| hyF , Lpar v;
    Lsur <- `q ∈ ℚ ⟹ [ ∃ k \, \< pr k ; q \> ∈ |f ]` / ℚ. // W.!=. -| hyF , Lpred , ↑∈𝕄 , ⋅∈𝕄 , +∈𝕄 , 𝕄0s , 1. , 2. v;
    Lfsub <- `|f ⊂_ 𝕄 ^^pr ℚ` -| hyF , Lsub v;
    LfS <- `|f ∈ 𝕄 →S ℚ` /// W.!=.!ℚ. -| Lfsub , Lfto , Luni , Lsur v;
    goal -| LfS p;
    goal -| W. , ax_s , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 h[fix];

articles3/3.book

`articles3/3.book`