未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
articles3/3b.book
ヘッダ
行番号
title 有理数の可算性（Calkin–Wilf） import 0-pa formel /common/default thmel /common/zf option review quick:true;
section Stern の数列 txt \({\rm fusc}\) は次の漸化式を満たす関数として仮定します（存在は示しません）。\(0, 1, 1, 2, 1, 3, 2, 3, 1, 4, \ldots\) と続く数列です。 word fusc prop fusc𝕄 <- `\\{ And fusc (0) = 0 \\ fusc (1) = 1 \\ n ∈ 𝕄 ⟹ fusc (2 ⋅ n) = fusc (n) \\ n ∈ 𝕄 ⟹ fusc (2 ⋅ n + 1) = fusc (n) + fusc (n suc) \\}` let/thm Lfusc <- `n ∈ 𝕄 ⟹ fusc (n) ∈ 𝕄 and (n {/}= 0 ⟹ fusc (n) {/}= 0)` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄 prf Lord <- `k ∈ 𝕄 ⟹ k < 2 ⋅ k + 1 and (k {/}= 0 ⟹ k < 2 ⋅ k and k suc < 2 ⋅ k + 1)` / <. / ≤. -| L2⋅ , Lpred , Lsuc+ , L0+ , +1 , +𝕄 , +∈𝕄 , 𝕄0s , 1. , 2. v; E0 <- `fusc (2 ⋅ 0) = 0 and 2 ⋅ 0 = 0` -| fusc𝕄 , *𝕄 , `2 ∈ 𝕄` p; E1 <- `k ∈ 𝕄 and fusc (k) ∈ 𝕄 and fusc (k) {/}= 0 ⟹ fusc (2 ⋅ k) ∈ 𝕄 and fusc (2 ⋅ k) {/}= 0` -| fusc𝕄 p; O0 <- `fusc (2 ⋅ 0 + 1) ∈ 𝕄 and fusc (2 ⋅ 0 + 1) {/}= 0` -| fusc𝕄 , *𝕄 , L0+ , `2 ∈ 𝕄` , suc𝕄 , 𝕄0s , 1. p; O1 <- `k ∈ 𝕄 and fusc (k) ∈ 𝕄 and fusc (k suc) ∈ 𝕄 and fusc (k suc) {/}= 0 ⟹ fusc (2 ⋅ k + 1) ∈ 𝕄 and fusc (2 ⋅ k + 1) {/}= 0` -| fusc𝕄 , L+=0 , +∈𝕄 p; Le <- `[ n ; k col ∈ 𝕄 ] and n = 2 ⋅ k and [ ∀ z ∈ 𝕄 . (z < n ⟹ fusc (z) ∈ 𝕄 and (z {/}= 0 ⟹ fusc (z) {/}= 0)) ] ⟹ fusc (n) ∈ 𝕄 and (n {/}= 0 ⟹ fusc (n) {/}= 0)` -| Lord , E0 , E1 , 𝕄0s v; Lo <- `[ n ; k col ∈ 𝕄 ] and n = 2 ⋅ k + 1 and [ ∀ z ∈ 𝕄 . (z < n ⟹ fusc (z) ∈ 𝕄 and (z {/}= 0 ⟹ fusc (z) {/}= 0)) ] ⟹ fusc (n) ∈ 𝕄 and (n {/}= 0 ⟹ fusc (n) {/}= 0)` -| Lord , O0 , O1 , suc𝕄 , 𝕄0s v; Ls <- `n ∈ 𝕄 and [ ∀ z ∈ 𝕄 . (z < n ⟹ fusc (z) ∈ 𝕄 and (z {/}= 0 ⟹ fusc (z) {/}= 0)) ] ⟹ fusc (n) ∈ 𝕄 and (n {/}= 0 ⟹ fusc (n) {/}= 0)` -| Lpar , Le , Lo p; Lfusc -| SIND𝕄[D_:=`\{ cls n | fusc (n) ∈ 𝕄 and (n {/}= 0 ⟹ fusc (n) {/}= 0) \}`] , Ls v; Lfusc -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄 h; br txt Calkin–Wilf：どの \(a, b\)（\(b \neq 0\)）も、ある \(n\) と \(g\) で \(a = g\,{\rm fusc}(n)\)、\(b = g\,{\rm fusc}(n+1)\) と書ける。 txt \(a+b\) についての強い帰納法：\(a = 0\) なら \(n = 0\)。\(b \le a\) なら \((a-b, b)\) から \(2n+1\) へ、\(a < b\) なら \((a, b-a)\) から \(2n\) へ（互除法を逆にたどる）。 let/thm LCW <- `[ a ; b col ∈ 𝕄 ] and b {/}= 0 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄 prf L2s <- `n ∈ 𝕄 ⟹ (2 ⋅ n + 1) suc = 2 ⋅ n suc` -| *𝕄 , +1 , +A , +𝕄 , ⋅∈𝕄 , `2 ∈ 𝕄` , 𝕄0s , 1. , 2. v; F2 <- `n ∈ 𝕄 ⟹ fusc (2 ⋅ n) = fusc (n) and fusc ((2 ⋅ n) suc) = fusc (n) + fusc (n suc)` -| fusc𝕄 , +1 , ⋅∈𝕄 , `2 ∈ 𝕄` p; F3 <- `n ∈ 𝕄 ⟹ fusc (2 ⋅ n + 1) = fusc (n) + fusc (n suc) and fusc ((2 ⋅ n + 1) suc) = fusc (n suc)` -| fusc𝕄 , L2s , 𝕄0s p; Lg <- `[ g ; x ; y col ∈ 𝕄 ] ⟹ g ⋅ y + g ⋅ x = g ⋅ (x + y)` -| Ldist , +C , ⋅∈𝕄 p; C0 <- `b ∈ 𝕄 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . 0 = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]` -| fusc𝕄 , *𝕄 , L⋅1 , 𝕄0s , 1. v; CL <- `[ a ; c col ∈ 𝕄 ] and [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and c = g ⋅ fusc (n suc) ] ] ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and c + a = g ⋅ fusc (n suc) ] ]` -| F2 , Lg , Lfusc , ⋅∈𝕄 , `2 ∈ 𝕄` , 𝕄0s v; CR <- `[ c ; b col ∈ 𝕄 ] and [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . c = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ] ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . c + b = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]` -| F3 , Ldist , Lfusc , ⋅∈𝕄 , +∈𝕄 , `2 ∈ 𝕄` , 𝕄0s , 1. v; SB <- `[ s ; a ; b col ∈ 𝕄 ] and [ ∀ z ∈ 𝕄 . (z < s ⟹ [ ∀ a ∈ 𝕄 . [ ∀ b ∈ 𝕄 . (a + b = z and b {/}= 0 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]) ] ]) ] and a + b = s and b {/}= 0 and a {/}= 0 and b ≤ a ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]` / ≤. -| CR , L<+ , +C , +∈𝕄 v; SC <- `[ s ; a ; b col ∈ 𝕄 ] and [ ∀ z ∈ 𝕄 . (z < s ⟹ [ ∀ a ∈ 𝕄 . [ ∀ b ∈ 𝕄 . (a + b = z and b {/}= 0 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]) ] ]) ] and a + b = s and b {/}= 0 and a {/}= 0 and a < b ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]` -| L<d , CL , L<+ , +C , +∈𝕄 v; Ls <- `s ∈ 𝕄 and [ ∀ z ∈ 𝕄 . (z < s ⟹ [ ∀ a ∈ 𝕄 . [ ∀ b ∈ 𝕄 . (a + b = z and b {/}= 0 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]) ] ]) ] ⟹ [ ∀ a ∈ 𝕄 . [ ∀ b ∈ 𝕄 . (a + b = s and b {/}= 0 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]) ] ]` -| C0 , SB , SC , Ltot v; LCW -| SIND𝕄[D_:=`\{ cls s | [ ∀ a ∈ 𝕄 . [ ∀ b ∈ 𝕄 . (a + b = s and b {/}= 0 ⟹ [ ∃ n ∈ 𝕄 . [ ∃ g ∈ 𝕄 . a = g ⋅ fusc (n) and b = g ⋅ fusc (n suc) ] ]) ] ] \}`] , Ls , +∈𝕄 v; LCW -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄 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\) については約分（÷K）だけを仮定します。 word - word ÷ word ℤ ℚ prop ℤ. <- `ℤ =_ \{ cls a | a ∈ 𝕄 or [ ∃ n ∈ 𝕄 . a = - n ] \}` prop ℚ. <- `ℚ =_ \{ a ÷ b Cls a ; b | a ∈ ℤ and b ∈ 𝕄 and b {/}= 0 \}` prop ÷K <- `\\{ And [ c ; a ; b col ∈ 𝕄 ] and c {/}= 0 ⟹ (c ⋅ a) ÷ (c ⋅ b) = a ÷ b \\ [ c ; a ; b col ∈ 𝕄 ] and c {/}= 0 ⟹ (- (c ⋅ a)) ÷ (c ⋅ b) = (- a) ÷ b \\}` newpage section 主定理 txt 偶数 \(2n\) に \({\rm fusc}(n) \div {\rm fusc}(n+1)\)、奇数 \(2n+1\) に \(-{\rm fusc}(n) \div {\rm fusc}(n+1)\) を対応させる（Calkin–Wilf の数え上げに符号を付けたもの）。 txt 有理数 \(\pm a \div b\) は、LCW で \(a = g\,{\rm fusc}(n)\)、\(b = g\,{\rm fusc}(n+1)\) と書いて約分すれば値に現れるので、この対応は全射。 thm `[ ∃ f \, f ∈ 𝕄 →S ℚ ]` ◀ W. , ax_s , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , fusc𝕄 , ÷K prf f_ := `\{ \< pr k ; q \> Cls k ; q | [ ∃ n ∈ 𝕄 . (k = 2 ⋅ n and q = fusc (n) ÷ fusc (n suc)) or (k = 2 ⋅ n + 1 and q = (- fusc (n)) ÷ fusc (n suc)) ] \}` ; hyF <- `|f =_ f_` ; Lsub <- `f_ ⊂_ 𝕄 ^^pr ℚ` //// W.!=. -| Lfusc , ⋅∈𝕄 , +∈𝕄 , suc𝕄 , `2 ∈ 𝕄` , 𝕄0s , 1. v; Lmem <- `\< pr k ; q \> ∈ |f ⟹ [ ∃ n ∈ 𝕄 . (k = 2 ⋅ n and q = fusc (n) ÷ fusc (n suc)) or (k = 2 ⋅ n + 1 and q = (- fusc (n)) ÷ fusc (n suc)) ]` -| hyF , pr:0 v; LV <- `[ n ; m col ∈ 𝕄 ] and ((k = 2 ⋅ n and q = fusc (n) ÷ fusc (n suc)) or (k = 2 ⋅ n + 1 and q = (- fusc (n)) ÷ fusc (n suc))) and ((k = 2 ⋅ m and r = fusc (m) ÷ fusc (m suc)) or (k = 2 ⋅ m + 1 and r = (- fusc (m)) ÷ fusc (m suc))) ⟹ q = r` -| L2K , L1K , Lne v; Luni <- `\< pr k ; q \> ∈ |f and \< pr k ; r \> ∈ |f ⟹ q = r` -| Lmem , LV v; Lfto <- `k ∈ 𝕄 ⟹ [ ∃ q \, \< pr k ; q \> ∈ |f ]` -| hyF , Lpar v; Lg0 <- `[ g ; y col ∈ 𝕄 ] and g ⋅ y {/}= 0 ⟹ g {/}= 0` -| L0⋅ p; S+ <- `[ a ; b col ∈ 𝕄 ] and b {/}= 0 ⟹ [ ∃ k \, \< pr k ; a ÷ b \> ∈ |f ]` -| hyF , LCW , ÷K , Lg0 , Lfusc , ⋅∈𝕄 , `2 ∈ 𝕄` , 𝕄0s v; S- <- `[ a ; b col ∈ 𝕄 ] and b {/}= 0 ⟹ [ ∃ k \, \< pr k ; (- a) ÷ b \> ∈ |f ]` -| hyF , LCW , ÷K , Lg0 , Lfusc , ⋅∈𝕄 , `2 ∈ 𝕄` , 𝕄0s v; Lsur <- `q ∈ ℚ ⟹ [ ∃ k \, \< pr k ; q \> ∈ |f ]` / ℚ. // W.!=. -| S+ , S- 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𝕄 , +𝕄 , *𝕄 , fusc𝕄 , ÷K h[fix];
表示（保存しません）
保存にはMatheliaへのログインが要ります。