book集

section 置換を動く点で分ける
txt 置換 \(f\) の動く点の集合を \(M(f) = \{x \mid f(x) \neq x\}\) とする。\(M(f) = A\) となる置換は、\(f \setminus \mathrm{id}\) で \(A\) の完全順列と1対1に対応する（逆は \(g \mapsto g \cup \mathrm{id}_{N \setminus A}\)）。
!let/thm LMg <- `A ⊂ N and [ ∀ g \, (g ∈ D ⟺ g ∈ A →IS A and g ∩ id _ A = ∅) ] and [ ∀ f \, (f ∈ F ⟺ f ∈ N →IS N and ^◁ (f ∖ id _ N) = A) ] ⟹ F =# D` ◀ W. , ax_s
prf hyA <- `|A ⊂ |N` ;
    hyD <- `[ ∀ g \, (g ∈ |D ⟺ g ∈ |A →IS |A and g ∩ id _ |A = ∅) ]` ;
    hyF <- `[ ∀ f \, (f ∈ |F ⟺ f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A) ]` ;
    LdA <- `|A ∩ (|N ∖ |A) = ∅ and |A ∪ (|N ∖ |A) = |N` / =. /// W.'!=. -| hyA / ⊂. p;
    Lφ <- `g ∈ |D ⟹ (g ∪ id _ (|N ∖ |A)) ∈ |N →IS |N` -| hyD , →IS∪ , id:0 , LdA p;
    Lg0 <- `g ∈ |D and p ∈ g ⟹ [ ∃ x ; y \, p = \< pr x ; y \> and x ∈ |A and y ∈ |A and x {/}= y ]` -| hyD /// W.'!=. , Lid∅ , pr:0 v;
    Lgm <- `g ∈ |D ⟹ (g ∪ id _ (|N ∖ |A)) ∖ id _ |N = g` / =. / ∖. / ∪. / id. / id. -| Lg0 , hyA / ⊂. , ∖. , pr:0 v;
    LgA <- `g ∈ |D ⟹ ^◁ (g) = |A` / =. /// W.'!=. -| hyD /// W.'!=. , pr:0 v;
    LeF <- `g ∈ |D ⟹ g ∪ id _ (|N ∖ |A) ∈ |F` -| hyF , Lφ , Lgm , LgA p;
    |K_ := `\{ \< pr g ; g ∪ id _ (|N ∖ |A) \> Cls g | g ∈ |D \}` ;
    hyK <- `|K =_ |K_` ;
    LKs <- `|K_ ⊂_ |D ^^pr |F` / ^^pr. -| LeF p;
    LKm <- `\< pr g ; f \> ∈ |K ⟺ g ∈ |D and f = g ∪ id _ (|N ∖ |A)` -| hyK , pr:0 p;
    Linj <- `g ∈ |D and g' ∈ |D and g ∪ id _ (|N ∖ |A) = g' ∪ id _ (|N ∖ |A) ⟹ g = g'` -| Lgm p;
    Lf1 <- `f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A ⟹ f = (f ∖ id _ |N) ∪ id _ (|N ∖ |A)` / =. /// W.'!=. -| pr:0 v;
    Lfs <- `f ∈ |N →IS |N ⟹ f ⊂ |N ^^pr |N` / →IS.' -| O p;
    LfM <- `^◁ (f ∖ id _ |N) = |A ⟹ (x ∈ |A ⟺ [ ∃ y \, \< pr x ; y \> ∈ f and \< pr x ; y \> {/}∈ id _ |N ])` / =. / ^◁. / ∖. -| O p;
    Lid <- `x ∈ |N ⟹ (\< pr x ; y \> ∈ id _ |N ⟺ x = y)` / id. -| pr:0 p;
    Lfx <- `f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A and x ∈ |N and x {/}∈ |A ⟹ \< pr x ; x \> ∈ f` -| LfM , Lid , Lfs / ⊂. / ^^pr. , →IS.' , ⊂. , ^^pr. , pr:0 v;
    LfA <- `f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A and \< pr x ; y \> ∈ f and x ∈ |A ⟹ y ∈ |A and y {/}= x` -| LfM , Lid , Lfs / ⊂. / ^^pr. , Lfx , hyA , →IS.' , ⊂. , ^^pr. , pr:0 v;
    LfB <- `f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A and y ∈ |A ⟹ [ ∃ x \, x ∈ |A and \< pr x ; y \> ∈ f ]` -| Lfx , Lfs / ⊂. / ^^pr. , hyA , →IS.' , ⊂. , ^^pr. , pr:0 v;
    Lfu <- `f ∈ |N →IS |N and \< pr x ; y \> ∈ f and \< pr x ; z \> ∈ f ⟹ y = z` / →IS.' / ⊂. / ^^pr. -| pr:0 v;
    Lfi <- `f ∈ |N →IS |N and \< pr x ; y \> ∈ f and \< pr z ; y \> ∈ f ⟹ x = z` / →IS.' / ⊂. / ^^pr. -| pr:0 v;
    Lft <- `f ∈ |N →IS |N and x ∈ |N ⟹ [ ∃ y \, \< pr x ; y \> ∈ f ]` / →IS.' -| O v;
    Lgp <- `f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A ⟹ (\< pr x ; y \> ∈ f ∖ id _ |N ⟺ \< pr x ; y \> ∈ f and x ∈ |A)` / ∖. -| LfA , Lfx , Lfu , Lid , Lfs / ⊂. / ^^pr. , pr:0 v;
    Lga <- `f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A ⟹ f ∖ id _ |N ⊂ |A ^^pr |A` / ⊂. / ^^pr. -| Lgp , LfA , Lfs / ⊂. / ^^pr. , ∖. , pr:0 v;
    Lgb <- `f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A ⟹ [ ∀ x ∈ |A . [ ∃！ y \, \< pr x ; y \> ∈ f ∖ id _ |N ] ]` -| Lgp , Lfu , Lft , hyA / ⊂. v;
    Lgc <- `f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A ⟹ [ ∀ y ∈ |A . [ ∃！ x \, \< pr x ; y \> ∈ f ∖ id _ |N ] ]` -| Lgp , LfB , Lfi v;
    Lgd <- `f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A ⟹ (f ∖ id _ |N) ∩ id _ |A = ∅` -| Lid∅ , Lgp , LfA p;
    Lf2 <- `f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A ⟹ f ∖ id _ |N ∈ |D` -| hyD , Lga , Lgb , Lgc , Lgd , →IS.' p;
    Lsur <- `f ∈ |F ⟹ [ ∃ g \, g ∈ |D and f = g ∪ id _ (|N ∖ |A) ]` -| hyF , Lf1 , Lf2 v;
    LK0 <- `|K ⊂ |D ^^pr |F` / ⊂. -| hyK , LKs p;
    LK1 <- `[ ∀ g ∈ |D . [ ∃！ f \, \< pr g ; f \> ∈ |K ] ]` -| LKm p;
    LK2 <- `[ ∀ f ∈ |F . [ ∃！ g \, \< pr g ; f \> ∈ |K ] ]` -| LKm , Lsur , Linj p;
    LDF <- `|D =# |F` / =#.' / →IS.' -| LK0 , LK1 , LK2 p;
    `|F =# |D` -| LDF , =#:X p;
    LMg -| W. , ax_s h[fix];
!let/thm LMd <- `A ⊂ N and A =# j and j ∈ 𝕄 and [ ∀ f \, (f ∈ F ⟺ f ∈ N →IS N and ^◁ (f ∖ id _ N) = A) ] ⟹ F =# der (j)` ◀ W. , ax_s , AxD
prf hyA <- `|A ⊂ |N` ;
    hyAj <- `|A =# |j` ;
    hyj <- `|j ∈ 𝕄` ;
    hyF <- `[ ∀ f \, (f ∈ |F ⟺ f ∈ |N →IS |N and ^◁ (f ∖ id _ |N) = |A) ]` ;
    LDj <- `[ ∃ D \, [ ∀ g \, (g ∈ D ⟺ g ∈ |A →IS |A and g ∩ id _ |A = ∅) ] and D =# der (|j) ]` -| der=# , hyAj , hyj v;
    `|F =# der (|j)` -| LMg , hyA , hyF , LDj , =#:T v;
    LMd -| W. , ax_s , AxD h[fix];
txt 動く点の集合は \(N\) の部分集合。
!let/thm LM⊂ <- `f ∈ N →IS N ⟹ ^◁ (f ∖ id _ N) ⊂ N` ◀ W.
prf LM⊂ / ⊂. / ^◁. / ∖. / →IS.' / ⊂. / ^^pr. -| pr:0 p; LM⊂ -| W. h;
txt 動く点が \(j\) 個の置換の全体 \(P\) は、動く点の集合（\(n\) の \(j\) 元部分集合）ごとに \(\mathrm{der}(j)\) 個ずつなので \(\mathrm{der}(j) \cdot n \mathrm{C} j\) 個（LΣg）。
!let/thm LEjT <- `n ∈ 𝕄 and j ∈ 𝕄 and [ ∀ f \, (f ∈ P ⟺ f ∈ n →IS n and ^◁ (f ∖ id _ n) =# j) ] and [ ∀ A \, (A ∈ T ⟺ A ⊂ n and A =# j) ] and T =# n choose j ⟹ P =# der (j) ⋅ (n choose j)` ◀ W. , ax_s , Ax1 , Ax+ , Ax⋅ , AxC , AxD
prf hyN <- `|n ∈ 𝕄` ;
    hyj <- `|j ∈ 𝕄` ;
    hyP <- `[ ∀ f \, (f ∈ |P ⟺ f ∈ |n →IS |n and ^◁ (f ∖ id _ |n) =# |j) ]` ;
    hyT <- `[ ∀ A \, (A ∈ |T ⟺ A ⊂ |n and A =# |j) ]` ;
    hyTc <- `|T =# |n choose |j` ;
    |R_ := `\{ \< pr f ; ^◁ (f ∖ id _ |n) \> Cls f | f ∈ |P \}` ;
    hyR <- `|R =_ |R_` ;
    LRs <- `|R_ ⊂_ |P ^^pr |T` / ^^pr. -| hyP , hyT , LM⊂ p;
    c1 <- `|R ⊂ |P ^^pr |T` / ⊂. -| hyR , LRs p;
    c2 <- `[ ∀ s ∈ |P . [ ∃！ e \, \< pr s ; e \> ∈ |R ] ]` -| hyR , pr:0 p;
    LFe <- `e ∈ |T and [ ∀ s \, (s ∈ G ⟺ \< pr s ; e \> ∈ |R) ] ⟹ G =# der (|j)` -| LMd , hyR , hyP , hyT , hyj , LM⊂ , =#:T , =#:X , pr:0 v;
    `|P =# der (|j) ⋅ (|n choose |j)` -| LΣc , c1 , c2 , LFe , hyTc , AxD&l , AxC&l , hyN , hyj v;
    LEjT -| W. , ax_s , Ax1 , Ax+ , Ax⋅ , AxC , AxD h[fix,lift];
!let/thm LEj <- `n ∈ 𝕄 and j ∈ 𝕄 and [ ∀ f \, (f ∈ P ⟺ f ∈ n →IS n and ^◁ (f ∖ id _ n) =# j) ] ⟹ P =# der (j) ⋅ (n choose j)` ◀ W. , ax_s , Ax1 , Ax+ , Ax⋅ , AxC , AxD
prf LEj -| LEjT , choose=# , =#:R v; LEj -| W. , ax_s , Ax1 , Ax+ , Ax⋅ , AxC , AxD h[lift];
section 主定理
txt どの置換も「動く点の集合（\(k\) 元）」と「その上の完全順列」の組に1通りに分かれるので、\(n! = \sum_{k=0}^{n} \mathrm{der}(k) \cdot n \mathrm{C} k\)（引き算の要らない形の包除）。置換を動く点の個数 \(k\) で分けて LΣg を使う。
thm `n ∈ 𝕄 ⟹ [ ∑ i ∈ (0 .. n) . der (i) ⋅ (n choose i) ] = n !` ◀ W. , ax_s , Ax1 , Ax+ , Ax⋅ , Ax! , AxC , AxD , AxΣ
prf hyN <- `|n ∈ 𝕄` ;
    |R_ := `\{ \< pr f ; k \> Cls f ; k | f ∈ |n →IS |n and k ∈ 0 .. |n and ^◁ (f ∖ id _ |n) =# k \}` ;
    hyR <- `|R =_ |R_` ;
    LRs <- `|R_ ⊂_ (|n →IS |n) ^^pr (0 .. |n)` / ^^pr. -| O p;
    d1 <- `|R ⊂ (|n →IS |n) ^^pr (0 .. |n)` / ⊂. -| hyR , LRs p;
    d2 <- `[ ∀ s ∈ (|n →IS |n) . [ ∃！ e \, \< pr s ; e \> ∈ |R ] ]` -| hyR , Lsz , LM⊂ , =#:R , L..𝕄 , L=#𝕄 , =#:T , =#:X , hyN , pr:0 v;
    Lt∈ <- `i ∈ 𝕄 ⟹ der (i) ⋅ (|n choose i) ∈ 𝕄` -| AxD&l , AxC&l , Ax⋅&l , hyN v;
    LGg <- `[ ∀ j ; y \, (\< pr j ; y \> ∈ f ⟺ j ∈ X and y = der (j) ⋅ (|n choose j)) ] and [ ∀ p ∈ f . [ ∃ j ; y \, p = \< pr j ; y \> ] ] and [ ∀ j ∈ X . j ∈ 𝕄 ] ⟹ f ∈ X → 𝕄` / →.' -| Lt∈ v;
    LG <- `X = 0 .. |n ⟹ ｢ fn i ↦ der (i) ⋅ (|n choose i) ｣ Rest _ X ∈ X → 𝕄` --| LGg , L..𝕄 , pr:0 v;
    LRm <- `X = 0 .. |n ⟹ (\< pr x ; y \> ∈ ｢ fn i ↦ der (i) ⋅ (|n choose i) ｣ Rest _ X ⟺ x ∈ X and y = der (x) ⋅ (|n choose x))` --| pr:0 v;
    Lfib <- `e ∈ 0 .. |n and [ ∀ s \, (s ∈ G ⟺ \< pr s ; e \> ∈ |R) ] ⟹ G =# der (e) ⋅ (|n choose e)` -| LEj , hyR , L..𝕄 , hyN , pr:0 v;
    d4 <- `X = 0 .. |n ⟹ [ ∀ e ; w \, (\< pr e ; w \> ∈ ｢ fn i ↦ der (i) ⋅ (|n choose i) ｣ Rest _ X ⟹ [ ∀ G \, ([ ∀ s \, (s ∈ G ⟺ \< pr s ; e \> ∈ |R) ] ⟹ G =# w) ]) ]` --| LRm , Lfib v;
    d5 <- `X = 0 .. |n ⟹ X =# |n + 1 and |n + 1 ∈ 𝕄` -| L..# , hyN , 𝕄1 p;
    LΣn <- `X = 0 .. |n ⟹ ∑ (｢ fn i ↦ der (i) ⋅ (|n choose i) ｣ Rest _ X) ∈ 𝕄 and (|n →IS |n) =# ∑ (｢ fn i ↦ der (i) ⋅ (|n choose i) ｣ Rest _ X)` --| LΣ∑ , d1 , d2 , LG , d4 , d5 v;
    LfX <- `X = 0 .. |n ⟹ [ ∑ i ∈ X . der (i) ⋅ (|n choose i) ] = |n !` --| LΣn , Ax!&r , Ax!&l , L=#𝕄 , =#:T , =#:X , hyN v;
    Lbn <- `X = 0 .. |n ⟹ ｢ fn i ↦ der (i) ⋅ (|n choose i) ｣ Rest _ X = ｢ fn i ↦ der (i) ⋅ (|n choose i) ｣ Rest _ (0 .. |n)` --| Lext v;
    Lfin <- `[ ∑ i ∈ (0 .. |n) . der (i) ⋅ (|n choose i) ] = |n !` --| LfX , Lbn v;
    goal -| W. , ax_s , Ax1 , Ax+ , Ax⋅ , Ax! , AxC , AxD , AxΣ h[fix,lift];
!txt 2026-10-15 整理のメモ：置換を動く点の個数で分けて LΣ∑（02）、その各部分を動く点の集合で分けて LΣc（02）で数える。以前の版（組 \(\{(0,f),(1,M(f))\}\) で表し、帰納法 LG0・LGs・LGind で数えた 273 行）から 103 行に。

articles2/88b.book

`articles2/88b.book`