book集

section 組合せの数の準備
br
word choose
prop choose𝕄 <- `\\{ And n ∈ 𝕄 ⟹ n choose 0 = 1 \\ k ∈ 𝕄 ⟹ 0 choose (k + 1) = 0 \\ [ n ; k col ∈ 𝕄 ] ⟹ (n + 1) choose (k + 1) = n choose k + n choose (k + 1) \\}`
let/thm choose∈𝕄 <- `[ n ; k col ∈ 𝕄 ] ⟹ n choose k ∈ 𝕄` ◀ W. , ax_s , +𝕄 , choose𝕄
prf Lb <- `[ ∀ k ∈ 𝕄 . 0 choose k ∈ 𝕄 ]` -| choose𝕄 , +1 , Lpred , `0 ∈ 𝕄` , `1 ∈ 𝕄` p;
    Ls <- `n ∈ 𝕄 and [ ∀ k ∈ 𝕄 . n choose k ∈ 𝕄 ] ⟹ [ ∀ k ∈ 𝕄 . n suc choose k ∈ 𝕄 ]` -| choose𝕄 , +1 , Lpred , +∈𝕄 , 𝕄1 , `1 ∈ 𝕄` v;
    choose∈𝕄 -| INDC[D_:=`\{ cls n | [ ∀ k ∈ 𝕄 . n choose k ∈ 𝕄 ] \}`] , Lb , Ls v;
    choose∈𝕄 -| W. , ax_s , +𝕄 , choose𝕄 h;
br

txt 1点を取り除くと個数は1つ減り（Lcan）、足すと1つ増える（Ladd）。
let/thm Lcan <- `Y ∪ \{ set a \} =# k + 1 and a {/}∈ Y and k ∈ 𝕄 ⟹ Y =# k` ◀ W. , ax_s , +𝕄
prf hyf <- `|f ∈ |Y ∪ \{ set |a \} →IS |k suc` ;
    hya <- `|a {/}∈ |Y` ;
    hyk <- `|k ∈ 𝕄` ;
    |g_ := `\{ \< pr x ; y \> Cls x ; y | x ∈ |Y and y ∈ |k and ( \< pr x ; y \> ∈ |f or ( \< pr x ; |k \> ∈ |f and \< pr |a ; y \> ∈ |f ) ) \}` ;
    hyg <- `|g =_ |g_` ;
    Lgs <- `|g_ ⊂_ |Y ^^pr |k` /// W.!=. -| O p;
    Lgi <- `|g ∈ |Y →IS |k` ///// W.'!=. -| hyg ///// W.'!=. , hyf ///// W.'!=. , hya , hyk , Lirr , pr:0 v;
    L1 <- `|Y =# |k` / =#.' -| Lgi p;
    Lf <- `f ∈ Y ∪ \{ set a \} →IS k suc and a {/}∈ Y and k ∈ 𝕄 ⟹ Y =# k` -| W. , ax_s h[fix];
    Lcan / =#.' -| Lf / =#.' , +1 p;
    Lcan -| W. , ax_s , +𝕄 h;
section 主定理
txt 自然数 \(n\) は集合 \(\{0, \dots, n-1\}\) なので（0-sn）、\(A \subset n\) は \(n\) 個の元から選んだ部分集合。
txt \(n\) の \(k\) 元部分集合全体を \(S\) とすると \(S\) は \(n \mathrm{C} k\) 個（\(n \mathrm{C} k\) はパスカルの漸化式 choose𝕄 で与える。階乗の式 \(n!/(k!\,(n-k)!)\) との関係はこの本では示していない）。
txt 主張は「そのような \(S\) がある」の形で書く（\(S\) は外延性で1つに決まる）。
txt \(k = 0\) なら空集合だけ。\(n = 0\) で \(k \ge 1\) なら1つも無い。
txt \(n+1\) の \(k+1\) 元部分集合は、\(n\) を含まないもの（\(n\) の \(k+1\) 元部分集合）と、\(B \cup \{n\}\)（\(B\) は \(n\) の \(k\) 元部分集合）に分かれる。
txt \(n \notin n\) なので \(B \mapsto B \cup \{n\}\) は単射で、2つの組は交わらない。
let/thm Lcomb <- `[ n ; k col ∈ 𝕄 ] ⟹ [ ∃ S \, [ ∀ A \, (A ∈ S ⟺ A ⊂ n and A =# k) ] and S =# n choose k ]` ◀ W. , ax_s , +𝕄 , choose𝕄
prf L#0 <- `A =# 0 ⟹ A = ∅` / =#.' //// W.'!=. -| O p;
    L0#s <- `k ∈ 𝕄 ⟹ ¬ ( 0 =# k suc )` / =#.' //// W.'!=. -| O p;
    Lk0 <- `n ∈ 𝕄 ⟹ [ ∀ A \, (A ∈ 1 ⟺ A ⊂ n and A =# 0) ] and 1 =# n choose 0` -| 1.' , L#0 , =#:R , choose𝕄 , 0. , ∅.' , ⊂. , =. v;
    Bs <- `j ∈ 𝕄 ⟹ [ ∀ A \, (A ∈ 0 ⟺ A ⊂ 0 and A =# j suc) ] and 0 =# 0 choose j suc` -| L#0 , L0#s , =#:R , choose𝕄 , +1 , 0. , 0.' , ∅.' , ⊂. , =. v;
    Lb <- `[ ∀ k ∈ 𝕄 . [ ∃ S \, [ ∀ A \, (A ∈ S ⟺ A ⊂ 0 and A =# k) ] and S =# 0 choose k ] ]` -| Lk0 , Bs , Lpred , `0 ∈ 𝕄` v;
    |Q_ := `\{ B ∪ \{ set |n \} Cls B | B ∈ |S0 and B ⊂ |n \}` ;
    |K_ := `\{ \< pr B ; B ∪ \{ set |n \} \> Cls B | B ∈ |S0 and B ⊂ |n \}` ;
    hyN <- `|n ∈ 𝕄` ;
    hyJ <- `|j ∈ 𝕄` ;
    hy1 <- `[ ∀ A \, (A ∈ |S1 ⟺ A ⊂ |n and A =# |j suc) ]` ;
    hy1c <- `|S1 =# |n choose |j suc` ;
    hy0 <- `[ ∀ A \, (A ∈ |S0 ⟺ A ⊂ |n and A =# |j) ]` ;
    hy0c <- `|S0 =# |n choose |j` ;
    hyQ <- `|Q =_ |Q_` ;
    hyK <- `|K =_ |K_` ;
    LQs <- `|Q_ ⊂_ ℘ (|n suc)` //// W.' -| O v;
    LKs <- `|K_ ⊂_ |S0 ^^pr |Q` /// W.!=. -| pr:0 , hyQ /// W.!=. p;
    LKi <- `|K ∈ |S0 →IS |Q` ///// W.'!=. -| hyK ///// W.'!=. , hyQ ///// W.'!=. , hy0 / ⊂. , pr:0 , LJ2 , Lirr , hyN p;
    LQ# <- `|S0 =# |Q` / =#.' -| LKi p;
    LM1a <- `A ∈ |Q ⟹ [ ∃ B \, B ∈ |S0 and B ⊂ |n and A = B ∪ \{ set |n \} ]` /// W.' -| hyQ /// W.' p;
    LM1b <- `B ∈ |S0 and B ⊂ |n ⟹ B ∪ \{ set |n \} ⊂ |n suc and B ∪ \{ set |n \} =# |j suc` -| hy0 , Ladd , +1 , Lirr , hyN , hyJ , ⊂. , suc.' , ∪. , set1. v;
    LM1 <- `A ∈ |Q ⟹ A ⊂ |n suc and A =# |j suc` -| LM1a , LM1b p;
    LM2 <- `A ∈ |S1 ⟹ A ⊂ |n suc and A =# |j suc` -| hy1 , ⊂. , suc.' p;
    LM3a <- `A ⊂ |n suc and A =# |j suc and |n {/}∈ A ⟹ A ∈ |S1` -| hy1 , ⊂. , suc.' p;
    LM3b <- `A ⊂ |n suc and A =# |j suc and |n ∈ A ⟹ A ∩ |n ∈ |S0 and A = (A ∩ |n) ∪ \{ set |n \}` -| hy0 , LB , Lcan , +1 , Lirr , hyN , hyJ , ∩. , ⊂. v;
    LM3c <- `B ∈ |S0 ⟹ B ∪ \{ set |n \} ∈ |Q` -| hyQ /// W.'!=. , hy0 / ⊂. p;
    LM3 <- `A ⊂ |n suc and A =# |j suc ⟹ A ∈ |Q or A ∈ |S1` -| LM3a , LM3b , LM3c p;
    LQd <- `|Q ∩ |S1 = ∅` / =. //// W.' -| hyQ //// W.' , hy1 / ⊂. , Lirr , hyN v;
    LS1 <- `[ ∃ S \, [ ∀ A \, (A ∈ S ⟺ A ⊂ |n suc and A =# |j suc) ] and S =# |n suc choose |j suc ]` -| LM1 , LM2 , LM3 , LQd , LQ# , hy0c , hy1c , ∪=#+ , =#:T , =#:X , choose𝕄 , +1 , choose∈𝕄 , hyN , hyJ , 𝕄1 , ∪. v;
    LS <- `[ n ; j col ∈ 𝕄 ] and [ ∀ A \, (A ∈ S1 ⟺ A ⊂ n and A =# j suc) ] and S1 =# n choose j suc and [ ∀ A \, (A ∈ S0 ⟺ A ⊂ n and A =# j) ] and S0 =# n choose j ⟹ [ ∃ S \, [ ∀ A \, (A ∈ S ⟺ A ⊂ n suc and A =# j suc) ] and S =# n suc choose j suc ]` -| W. , ax_s , +𝕄 , choose𝕄 h[fix];
    Ls <- `n ∈ 𝕄 and [ ∀ k ∈ 𝕄 . [ ∃ S \, [ ∀ A \, (A ∈ S ⟺ A ⊂ n and A =# k) ] and S =# n choose k ] ] ⟹ [ ∀ k ∈ 𝕄 . [ ∃ S \, [ ∀ A \, (A ∈ S ⟺ A ⊂ n suc and A =# k) ] and S =# n suc choose k ] ]` -| Lk0 , LS , Lpred , 𝕄1 v;
    Lcomb -| INDC[D_:=`\{ cls n | [ ∀ k ∈ 𝕄 . [ ∃ S \, [ ∀ A \, (A ∈ S ⟺ A ⊂ n and A =# k) ] and S =# n choose k ] ] \}`] , Lb , Ls v;
    Lcomb -| W. , ax_s , +𝕄 , choose𝕄 h;

articles2/58.book

`articles2/58.book`