# 排列與組合：以計數證明 P(n,k)=n!/(n−k)! 與 C(n,k)=n!/(k!(n−k)!)

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-permutation-combination/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-permutation-combination-01 · production-20261019-adopted-96



## 目標與範圍

設 X 是恰有 n 個相異物件的集合，n、k 為自然數且 0≤k≤n，選取無放回、不重複。證明：從 X 有序選取 k 個的方法數 P(n,k)=n!/(n−k)!，無序選取 k 個的方法數 C(n,k)=n!/(k!(n−k)!)，且 k=0 時兩者都等於 1。最後以 X={a,b,c,d,e}、k=3 算出 P(5,3)=60 與 C(5,3)=10。

只在 MKO 的模型內工作：物件相異、無放回、不重複、0≤k≤n，排列區分順序、組合忽略順序。以有限集合的互斥聯集計數與對 k 的歸納證明兩個公式。不處理重複選取、不可區分物件、環形排列或附加限制（MKO 指出它們需要不同的計數模型）；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- finite_counting_basics
- nat_induction
- frac_rules
- numeric_evaluation


- G1 — X 是恰有 n 個相異元素的有限集合；n、k∈ℕ（ℕ 含 0），0≤k≤n；選取無放回且不可重複（MKO 假設 a1）。
- G2 — 有序選取 k 個是 X 中兩兩相異元素的 k 元組 (x_i)_{i=1}^{k}，所成集合記為 𝒫_k(X)，P(n,k)=|𝒫_k(X)|；無序選取 k 個是 X 的 k 元子集合，所成集合記為 𝒞_k(X)，C(n,k)=|𝒞_k(X)|。k=0 時空元組與空集合各計為一種選取（MKO 假設 a2）。
- G3 — 例子：X={a,b,c,d,e}（五個相異字母），k=3。


- X — 恰有 n 個相異物件的有限集合
- \mathcal{P}_k(X) — X 中 k 個兩兩相異元素的 k 元組（有序選取）所成的集合
- \mathcal{C}_k(X) — X 的 k 元子集合（無序選取）所成的集合
- P(n,k),\ C(n,k) — 上述兩個集合的元素個數
- \operatorname{set}(t) — 元組 t 的各項所成的集合
- t^\frown x — 在元組 t 後面接上一項 x
- \sigma — 忘記順序的映射 t↦set(t)
- m! — 階乘：0!=1，(m+1)!=(m+1)·m!





## 規則與來源


- finite_counting_basics · prerequisite — 有限計數：互斥有限集合 A、B 有 |A∪B|=|A|+|B|；|A×B|=|A|·|B|；有限集之間存在雙射 ⇔ 元素個數相同。
- nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- imp_intro · prerequisite — →引入（釋放假設）：若在暫時假設 P 的作用域中推出 Q，則得到 P⇒Q；此後 P 不再可當作已知使用。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- mko_perm_comb · cited — 對自然數 n、k 且 0≤k≤n，由 n 個相異物件無放回選取 k 個的排列數為 P(n,k)=n!/(n−k)!，組合數為 C(n,k)=n!/(k!(n−k)!)；k=0 時兩者均為 1。 · mko-permutation-combination
- mko_factorial_def · cited — 函數 F:ℕ→ℕ 由 F(0)=1 與 F(m+1)=(m+1)F(m) 唯一遞迴決定；慣用記號為 m!。 · mko-factorial
- tuple_eq · prerequisite — 有限元組：兩個 k 元組相等當且僅當每個位置的項都相等；0 元組只有空元組 ()；對 k 元組 t 與物件 x，t⌢x 是前 k 項為 t、第 k+1 項為 x 的元組；每個 (k+1) 元組恰可唯一寫成 t⌢x，其中 t 是它的前 k 項、x 是它的最後一項。
- disjoint_union_count · prerequisite — 若有限集合是有限多個兩兩互斥的有限集合 B_j（j∈J，J 有限）的聯集，則其元素個數是 Σ_{j∈J}|B_j|；特別地，若每個 |B_j|=c，則為 |J|·c。這是 finite_counting_basics 的兩集合情形對集合個數歸納所得。
- L_fact_pos · lemma — 對每個自然數 m，m!≥1；特別地 m!≠0。
- L_complement_count · lemma — 若 Y 是有限集合且 A⊆Y，則 |Y∖A|=|Y|−|A|。
- L_same_size_subset · lemma — 若 A 是有限集合、B⊆A 且 |B|=|A|，則 B=A。





## 逐步主鏈

S01 · definition操作前

\text{ordered and unordered selections of }k\text{ objects from }X

操作後

P(n,k)=|\mathcal{P}_k(X)|,\quad C(n,k)=|\mathcal{C}_k(X)|

條件：0\le k\le n

規則：def_intro · 依賴：G1, G2

葉節點依據：def_intro + mko_perm_comb

把兩種計數對象寫成集合。依 MKO 的假設，有序選取是 X 中 k 個兩兩相異元素的 k 元組 (x_i)_{i=1}^{k}，順序不同就是不同的選取；無序選取是 X 的 k 元子集合，只記錄選了哪些物件。P(n,k)、C(n,k) 分別是這兩個集合的元素個數。之後要證明的是這兩個個數等於 MKO 的公式，而不是把公式當成定義。



S02 · implies操作前

m!\ (m\in\mathbb{N})

操作後

m!\geq 1,\ \text{hence}\ m!\neq 0

條件：m\in\mathbb{N}

規則：L_fact_pos · 依賴：mko_factorial_def

葉節點依據：nat_induction + mko_factorial_def + order_basics

後面要除以 n!、(n−k)! 與 k!，所以先確定階乘從不為零。依引理 L_fact_pos，每個 m! 都至少是 1；以歸納完成的證明在 S02.1 與 S02.2。



S03 · induction_base操作前

\mathcal{P}_0(X)

操作後

\mathcal{P}_0(X)=\{()\},\quad |\mathcal{P}_0(X)|=1=\frac{n!}{(n-0)!}

條件：n!\neq 0

規則：tuple_eq · 依賴：G1, G2, S02, tuple_eq

葉節點依據：tuple_eq + frac_rules + L_fact_pos

0 元組只有空元組 ()；它沒有任何項，「兩兩相異」自動成立，所以 𝒫_0(X)={()}，恰有 1 個元素。另一方面 n!/(n−0)!=n!/n!=1，這個除法需要 n!≠0（S02）。這是對 k 歸納的起點，也就是 MKO 所說「空排列有一種」。



S04 · implies操作前

\mathcal{P}_{k+1}(X)\quad(k+1\le n)

操作後

\mathcal{P}_{k+1}(X)=\bigcup_{t\in\mathcal{P}_k(X)}E(t),\quad E(t)=\{t^\frown x\mid x\in X\setminus\operatorname{set}(t)\},\ \text{pairwise disjoint}

條件：k+1\le n

規則：set_extensionality · 依賴：G2, tuple_eq

葉節點依據：set_extensionality + tuple_eq + set_operations_def

固定 k 使 k+1≤n。把每個 (k+1) 元有序選取按它的前 k 項分類：E(t) 收集以 t 開頭、再接一個不在 t 中的物件的元組。子步 S04.1、S04.2 證明兩個方向的包含，S04.3 證明各類互斥。



S05 · implies操作前

E(t)\quad(t\in\mathcal{P}_k(X))

操作後

|E(t)|=n-k\geq 1

條件：k+1\le n

規則：L_complement_count · 依賴：G1, G2, S04

葉節點依據：L_complement_count + finite_counting_basics + injective_surjective_def

每一類 E(t) 都恰有 n−k 個元素，與 t 是哪個元組無關；這是可以寫成乘積的關鍵（計數原理 MKO 要求每一階段的可選數已明確）。證明分三個子步：補集計數（S05.1）、set(t) 恰有 k 個元素（S05.2）、x↦t⌢x 是雙射（S05.3）。因 k+1≤n，n−k≥1。



S06 · implies操作前

\mathcal{P}_{k+1}(X)=\bigcup_{t\in\mathcal{P}_k(X)}E(t)

操作後

|\mathcal{P}_{k+1}(X)|=|\mathcal{P}_k(X)|\cdot(n-k)

條件：k+1\le n

規則：disjoint_union_count · 依賴：S04, S04.3, S05

葉節點依據：disjoint_union_count + finite_counting_basics

S04 把 𝒫_{k+1}(X) 寫成以 t∈𝒫_k(X) 為索引、兩兩互斥的類 E(t) 的聯集，S05 說每一類都恰有 n−k 個元素。依 disjoint_union_count（c=n−k），總數是 |𝒫_k(X)|·(n−k)。這就是 MKO 所說「每次可選數依次為 n、n−1，以此類推」的嚴格形式：第 k+1 次選取時有 n−k 個選項。



S07 · induction_step操作前

|\mathcal{P}_k(X)|=\frac{n!}{(n-k)!}

操作後

|\mathcal{P}_{k+1}(X)|=\frac{n!}{(n-(k+1))!}

條件：k+1\le n

規則：frac_rules · 依賴：S06, S02, mko_factorial_def

葉節點依據：frac_rules + mko_factorial_def + L_fact_pos

設歸納假設 |𝒫_k(X)|=n!/(n−k)! 且 k+1≤n。由 S06，|𝒫_{k+1}(X)|=n!(n−k)/(n−k)!。子步 S07.1 把 (n−k)! 拆成 (n−k)·(n−k−1)!，S07.2 約去公因子 n−k，得到 n!/(n−(k+1))!。



S08 · implies操作前

Q(k):\ k\le n\Rightarrow|\mathcal{P}_k(X)|=\frac{n!}{(n-k)!}

操作後

P(n,k)=\frac{n!}{(n-k)!}\quad\text{for all}\ 0\le k\le n

條件：無

規則：nat_induction · 依賴：S03, S07

葉節點依據：nat_induction + forall_intro + imp_intro

對 k 歸納命題 Q(k)：「若 k≤n，則 |𝒫_k(X)|=n!/(n−k)!」。Q(0) 是 S03。設 Q(k) 成立：若 k+1≤n，則 k≤n，由 Q(k) 得 |𝒫_k(X)|=n!/(n−k)!，再由 S07 得 Q(k+1)；若 k+1>n，Q(k+1) 的前件不成立，Q(k+1) 自動為真。依歸納原理所有 k 都有 Q(k)。證明只用到 |X|=n 與元素相異，沒有用到 X 的具體元素，所以對每個 n 元集合都成立（forall_intro）。



S09 · definition操作前

t\in\mathcal{P}_k(X)

操作後

\sigma(t)=\operatorname{set}(t)\in\mathcal{C}_k(X)

條件：無

規則：function_def · 依賴：G2, S05.2

葉節點依據：function_def + def_intro

定義 σ:𝒫_k(X)→𝒞_k(X)，把有序選取送到它所選物件的集合，也就是「忘記順序」。σ 有定義：依 S05.2 的推理，set(t) 是 X 的子集合且恰有 k 個元素，所以 set(t)∈𝒞_k(X)，而且每個 t 只對應一個集合。



S10 · implies操作前

\sigma^{-1}(\{A\})\quad(A\in\mathcal{C}_k(X))

操作後

\sigma^{-1}(\{A\})=\mathcal{P}_k(A)

條件：A\subseteq X,\ |A|=k

規則：set_extensionality · 依賴：S09

葉節點依據：set_extensionality + image_preimage_def + L_same_size_subset

對每個 k 元子集合 A，被 σ 送到 A 的有序選取，恰好是 A 中 k 個相異元素的 k 元組，也就是 A 的各種排序。兩個方向的包含見 S10.1 與 S10.3，S10.2 證明所需的有限集合引理。



S11 · theorem_application操作前

|\sigma^{-1}(\{A\})|=|\mathcal{P}_k(A)|

操作後

|\sigma^{-1}(\{A\})|=\frac{k!}{(k-k)!}=\frac{k!}{0!}=k!

條件：|A|=k

規則：forall_elim · 依賴：S08, S10

葉節點依據：forall_elim + mko_factorial_def + numeric_evaluation

S08 對每個 n 元集合與每個 0≤k≤n 成立。把它用在 k 元集合 A 上（n 換成 k，選取個數仍是 k，條件 0≤k≤k 成立），得 |𝒫_k(A)|=k!/(k−k)!=k!/0!=k!，因 0!=1。所以每個 k 元子集合恰有 k! 種排序，這就是 MKO 所說除以 k! 的依據。



S12 · implies操作前

\mathcal{P}_k(X)=\bigcup_{A\in\mathcal{C}_k(X)}\sigma^{-1}(\{A\})

操作後

P(n,k)=C(n,k)\cdot k!

條件：無

規則：disjoint_union_count · 依賴：S09, S10, S11

葉節點依據：disjoint_union_count + function_def + image_preimage_def

每個 t∈𝒫_k(X) 恰屬於一個纖維，即 σ^{-1}({σ(t)})（σ 是函數，只給 t 一個像），所以這些纖維兩兩互斥且聯集是 𝒫_k(X)。每個纖維恰有 k! 個元素（S11），纖維共有 |𝒞_k(X)|=C(n,k) 個。依 disjoint_union_count（c=k!），P(n,k)=C(n,k)·k!。



S13 · equivalent操作前

P(n,k)=C(n,k)\cdot k!

操作後

C(n,k)=\frac{P(n,k)}{k!}=\frac{n!}{k!\,(n-k)!}

條件：k!\neq 0

規則：mul_inverse_nonzero · 依賴：S12, S08, S02

葉節點依據：mul_inverse_nonzero + frac_rules + eq_replace + L_fact_pos

因 k!≠0（S02），兩邊同乘 1/k! 得 C(n,k)=P(n,k)/k!；再代入 S08 的 P(n,k)=n!/(n−k)!，依 frac_rules 得 n!/(k!(n−k)!)。



S14 · implies操作前

k=0

操作後

P(n,0)=\frac{n!}{n!}=1,\quad C(n,0)=\frac{n!}{0!\,n!}=1,\quad \mathcal{C}_0(X)=\{\varnothing\}

條件：0!=1; n!\neq 0

規則：forall_elim · 依賴：S08, S13, G2

葉節點依據：forall_elim + mko_factorial_def + frac_rules

代入 k=0：P(n,0)=n!/n!=1，C(n,0)=n!/(0!·n!)=n!/n!=1（0!=1）。直接看集合也一致：沒有元素的子集合只有空集合，所以 𝒞_0(X)={∅}，空選取計為一種，正如 MKO 假設 a2；n=0（X 為空）時也成立。



S15 · implies操作前

n=5,\ k=3

操作後

P(5,3)=60,\quad C(5,3)=10,\quad 10\cdot 3!=60

條件：0\le 3\le 5

規則：forall_elim · 依賴：G3, S06, S08, S13

葉節點依據：forall_elim + numeric_evaluation

代入 n=5、k=3：P(5,3)=5!/2!=120/2=60，與 S06 的遞推 1、5、20、60（依次乘 5、4、3）一致；C(5,3)=5!/(3!·2!)=120/12=10。核對 S12：10·3!=60。以 A={a,b,c} 為例，它的纖維恰是 6 個有序選取 (a,b,c)、(a,c,b)、(b,a,c)、(b,c,a)、(c,a,b)、(c,b,a)，而 3!=6。







## 局部子步與引理

S02.1 · induction_base操作前

0!

操作後

0!=1\geq 1

條件：無

規則：mko_factorial_def · 依賴：mko_factorial_def

葉節點依據：mko_factorial_def

依定義 F(0)=1，所以 0!=1≥1。0! 是 1，不是 0；這正是階乘 MKO 提醒的常見誤解。



S02.2 · induction_step操作前

m!\geq 1

操作後

(m+1)!=(m+1)\,m!\geq m!\geq 1

條件：m\geq 0

規則：order_basics · 依賴：S02.1, mko_factorial_def, order_basics

葉節點依據：order_basics + mko_factorial_def + nat_induction

設 m!≥1。由遞迴 (m+1)!=(m+1)·m!。因 m≥0，(m+1)·m!−m!=m·m!≥0（兩個非負數的乘積非負），所以 (m+1)!≥m!≥1。依歸納原理，S02.1 與 S02.2 合起來對所有 m 證得引理 L_fact_pos。



S04.1 · implies操作前

u\in\mathcal{P}_{k+1}(X)

操作後

u=t^\frown x,\ t\in\mathcal{P}_k(X),\ x\in X\setminus\operatorname{set}(t)

條件：無

規則：tuple_eq · 依賴：G2, tuple_eq

葉節點依據：tuple_eq + set_operations_def + subset_def

任取 u∈𝒫_{k+1}(X)。依 tuple_eq，u=t⌢x，t 是 u 的前 k 項、x 是最後一項。t 的項都是 u 的項，所以在 X 中且兩兩相異，t∈𝒫_k(X)。x 與 u 的其他每一項都不同，也就是 x∉set(t)，所以 x∈X∖set(t)，u∈E(t)。



S04.2 · implies操作前

t\in\mathcal{P}_k(X),\ x\in X\setminus\operatorname{set}(t)

操作後

t^\frown x\in\mathcal{P}_{k+1}(X)

條件：x\notin\operatorname{set}(t)

規則：tuple_eq · 依賴：G2, tuple_eq, S04.1

葉節點依據：tuple_eq + set_operations_def + set_extensionality

反過來，設 t∈𝒫_k(X)、x∈X 且 x∉set(t)。t⌢x 的前 k 項兩兩相異，最後一項 x 又不等於前面任何一項，所以 k+1 項兩兩相異且都在 X 中，t⌢x∈𝒫_{k+1}(X)。S04.1 與 S04.2 合起來，依 set_extensionality 得到 S04 的集合等式。



S04.3 · implies操作前

t^\frown x=s^\frown y

操作後

t=s\ \land\ x=y

條件：無

規則：tuple_eq · 依賴：tuple_eq

葉節點依據：tuple_eq + and_intro_elim

若 t⌢x=s⌢y，兩個元組逐位相等：前 k 項給出 t=s，最後一項給出 x=y。所以 t≠s 時 E(t) 與 E(s) 沒有共同元素；同一個 E(t) 中，不同的 x 給出不同的元組。



S05.1 · implies操作前

A\subseteq Y,\ Y\ \text{finite}

操作後

|Y\setminus A|=|Y|-|A|

條件：A\subseteq Y

規則：finite_counting_basics · 依賴：finite_counting_basics, set_operations_def

葉節點依據：finite_counting_basics + set_operations_def + eq_congruence

因 A⊆Y，Y=A∪(Y∖A)，而且 A 與 Y∖A 互斥（Y∖A 的元素不在 A 中）。依 finite_counting_basics，|Y|=|A|+|Y∖A|；兩邊同減 |A| 得 |Y∖A|=|Y|−|A|。這證得引理 L_complement_count。



S05.2 · implies操作前

t=(x_i)_{i=1}^{k}\in\mathcal{P}_k(X)

操作後

|\operatorname{set}(t)|=k,\quad |X\setminus\operatorname{set}(t)|=n-k

條件：無

規則：finite_counting_basics · 依賴：G2, S05.1

葉節點依據：injective_surjective_def + finite_counting_basics + L_complement_count

映射 i↦x_i 從位置集合 {i∈ℕ ∣ 1≤i≤k} 到 set(t) 是滿射（set(t) 就是各項的集合），也是單射（各項兩兩相異）。依 finite_counting_basics 的雙射計數，|set(t)|=k。又 set(t)⊆X，依 S05.1（Y=X、A=set(t)），|X∖set(t)|=n−k。這個推理對任何 t∈𝒫_k(X) 都成立，後面 S09、S10.3 也會用到。



S05.3 · implies操作前

x\mapsto t^\frown x:\ X\setminus\operatorname{set}(t)\to E(t)

操作後

|E(t)|=|X\setminus\operatorname{set}(t)|=n-k

條件：無

規則：injective_surjective_def · 依賴：S04.3, S05.2

葉節點依據：injective_surjective_def + finite_counting_basics

依 E(t) 的定義，它的每個元素都是某個 x∈X∖set(t) 的 t⌢x，所以這個映射是滿射；依 S04.3，t⌢x=t⌢y 推出 x=y，所以是單射。有雙射的兩個有限集合元素個數相同，故 |E(t)|=n−k。



S07.1 · equivalent操作前

(n-k)!

操作後

(n-k)\cdot(n-k-1)!

條件：n-k-1\in\mathbb{N}

規則：mko_factorial_def · 依賴：mko_factorial_def

葉節點依據：mko_factorial_def + eq_replace

令 m=n−k−1；因 k+1≤n，m 是自然數，而且 n−k=m+1。依遞迴 F(m+1)=(m+1)F(m)，(n−k)!=(n−k)·(n−k−1)!。



S07.2 · equivalent操作前

\frac{n!\,(n-k)}{(n-k)\cdot(n-k-1)!}

操作後

\frac{n!}{(n-k-1)!}=\frac{n!}{(n-(k+1))!}

條件：n-k\neq 0; (n-k-1)!\neq 0

規則：frac_rules · 依賴：S07.1, S02

葉節點依據：frac_rules + L_fact_pos + eq_replace

依 frac_rules 中「分子分母同乘一個非零數，分數不變」的規則，把非零公因子 n−k 從分子與分母約去；(n−k−1)!≠0 由 S02 保證。最後 n−k−1=n−(k+1)。



S10.1 · implies操作前

t\in\mathcal{P}_k(X),\ \sigma(t)=A

操作後

t\in\mathcal{P}_k(A)

條件：無

規則：image_preimage_def · 依賴：S09, image_preimage_def

葉節點依據：image_preimage_def + def_unfold

若 σ(t)=A，t 的每一項都在 set(t)=A 中，各項又兩兩相異，所以 t 是 A 中 k 個相異元素的 k 元組，t∈𝒫_k(A)。



S10.2 · implies操作前

B\subseteq A,\ |B|=|A|,\ A\ \text{finite}

操作後

B=A

條件：A\ \text{finite}

規則：L_complement_count · 依賴：S05.1, set_operations_def

葉節點依據：L_complement_count + set_extensionality + set_operations_def

由 L_complement_count（S05.1，取 Y=A），|A∖B|=|A|−|B|=0，所以 A∖B 是空集合：A 的每個元素都在 B 中，A⊆B。連同 B⊆A，依 set_extensionality 得 B=A。這證得引理 L_same_size_subset。



S10.3 · implies操作前

t\in\mathcal{P}_k(A)

操作後

t\in\mathcal{P}_k(X)\ \land\ \sigma(t)=A

條件：A\subseteq X

規則：L_same_size_subset · 依賴：S05.2, S10.2, G2

葉節點依據：L_same_size_subset + subset_def + set_extensionality

設 t∈𝒫_k(A)。因 A⊆X，t 也是 X 中相異元素的 k 元組，t∈𝒫_k(X)。依 S05.2 的推理 |set(t)|=k=|A|，而且 set(t)⊆A；依 L_same_size_subset，set(t)=A，即 σ(t)=A。S10.1 與 S10.3 合起來給出 σ^{-1}({A})=𝒫_k(A)。







## 逐步反向審查


- S15 · premise_audit · G3, S08, S13, numeric_evaluation — 這是一般公式的一個實例，可獨立重算（N1 至 N6、N9、N10）；它不能取代 S03 到 S13 的一般證明。
- S14 · premise_audit · S08, S13, forall_elim, mko_factorial_def — 需要 0!=1 與 n!≠0；若誤把 0! 當 0，C(n,0) 會變成除以零。
- S13 · inverse_equivalence · mul_inverse_nonzero, S02, frac_rules — 乘 1/k! 與乘 k! 互為反運算，前提 k!≠0；代入 S08 是等值代換，雙向成立。
- S12 · premise_audit · S09, S11, disjoint_union_count, function_def — 需要每個纖維大小都是 k!；若物件不可區分，不同選取的排序數可能不同，就不能寫成乘積。
- S11 · premise_audit · S08, S10, forall_elim, mko_factorial_def — 代入 S08 需要 A 的元素相異且 |A|=k；所用的是已證的一般結論，不是對某個例子的再計算。
- S10.3 · premise_audit · S05.2, S10.2, L_same_size_subset, set_extensionality — 關鍵是 set(t) 已有 |A| 個元素，因此不可能是 A 的真子集合；這依賴 A 有限。
- S10.2 · premise_audit · S05.1, set_extensionality, set_operations_def — 需要 A 有限；對無限集合，真子集合可以與原集合之間有雙射（例如偶數與 ℕ），這個引理就不成立。
- S10.1 · premise_audit · S09, image_preimage_def — 只用 set(t) 的定義；反向包含在 S10.3。
- S10 · premise_audit · S09, set_extensionality, image_preimage_def — 集合相等需要兩個方向的包含，在下列子步中逐一證明；只證一個方向不夠。
- S09 · premise_audit · G2, S05.2, function_def — 需要每個 t 的像確實在 𝒞_k(X) 中，這依賴各項兩兩相異。若有重複項，set(t) 的元素少於 k 個，σ 就不落在 𝒞_k(X)。
- S08 · sufficient_goal_reduction · S03, S07, nat_induction, forall_intro — 目標 G：0≤k≤n 時 P(n,k)=n!/(n−k)!。足夠條件 H：Q(0) 且對每個 k 有 Q(k)⇒Q(k+1)；H⇒G 由歸納原理。H 由 S03 與 S07 正向證成，沒有把 G 當作前提。
- S07.2 · inverse_equivalence · frac_rules, S02 — 約分與擴分互為反運算，前提是公因子 n−k 非零；若 n−k=0，約分不合法。
- S07.1 · inverse_equivalence · mko_factorial_def, eq_replace — 兩邊是同一個數的兩種寫法，可以雙向代換；條件是 n−k≥1，若 n−k=0，(n−k−1)! 沒有定義。
- S07 · premise_audit · S06, S02, frac_rules — 需要歸納假設、k+1≤n（使 n−k−1 是自然數）與分母非零（S02）；本步只由 k 推到 k+1。
- S06 · premise_audit · S04, S04.3, S05, disjoint_union_count — 需要互斥（否則重複計數）與每類大小相同（否則和不能寫成乘積）；兩者分別由 S04.3 與 S05 提供。
- S05.3 · premise_audit · S04.3, S05.2, injective_surjective_def, finite_counting_basics — 單射與滿射兩者都需要；只有其一不足以推出元素個數相等。
- S05.2 · premise_audit · G2, finite_counting_basics, injective_surjective_def, S05.1 — 「兩兩相異」保證單射；若有重複項，set(t) 會少於 k 個元素。
- S05.1 · premise_audit · finite_counting_basics, set_operations_def, eq_congruence — 需要 A⊆Y；若 A 不是 Y 的子集合，Y=A∪(Y∖A) 不成立，公式也會錯。
- S05 · premise_audit · L_complement_count, G1, finite_counting_basics — 需要 E(t) 的大小不依賴 t；若後續可選數隨前面的選擇改變，就不能直接相乘。
- S04.3 · premise_audit · tuple_eq — 只用元組相等的逐位條件；結論同時用於各類互斥（S06）與 S05.3 的單射。
- S04.2 · premise_audit · tuple_eq, set_operations_def, set_extensionality — 需要 x∉set(t)；這正是 E(t) 的定義要求 x 取自 X∖set(t) 的原因。
- S04.1 · premise_audit · G2, tuple_eq, set_operations_def — 用到 u 的各項兩兩相異；若允許重複，x 可能落在 set(t) 中，這個包含就不成立。
- S04 · premise_audit · G2, tuple_eq, set_extensionality — 集合相等需要兩個方向的包含，互斥另需證明；三者都在後面的子步中證成，只證一個方向不夠。
- S03 · premise_audit · tuple_eq, S02 — 需要「0 元組唯一」與 n!≠0；本步不依賴 X 的具體元素，n=0 時也成立。
- S02.2 · premise_audit · mko_factorial_def, order_basics, nat_induction — 需要歸納假設 m!≥1 與 m≥0；結論只由 m 推到 m+1，不宣稱反向。
- S02.1 · premise_audit · mko_factorial_def — 只用定義的第一條，不需其他前提。
- S02 · premise_audit · L_fact_pos, mko_factorial_def — 只需階乘的遞迴定義與歸納法；不宣稱反向（由 m!≥1 推回遞迴式）。
- S01 · premise_audit · G1, G2, def_intro, mko_perm_comb — 此步只命名，不推出新事實。它依賴物件相異（否則「兩兩相異」無從判定）與無放回（元組中不重複）；若改為可重複選取，𝒫_k(X) 的定義就不同，後面的證明也不適用。





## 錯誤控制與反例

先判斷順序、相異與放回MKO 指出的常見誤解是不先判斷條件就套公式。從 {a,b,c,d,e} 選 3 個：若區分順序且不可重複（例如分別選會長、副會長、秘書），用 P(5,3)=60；若只看選了誰（三人小組），用 C(5,3)=10；若可重複（三位字母密碼，字母可重複使用），每位都有 5 種，共 5³=125，P 與 C 都不適用。本稿每一步都依賴「相異」與「無放回」：S04.1 需要 x 不在 t 中，S05.2 需要各項兩兩相異。

除以 k! 需要每個子集合恰有 k! 種排序S12 能寫成 C(n,k)·k! 是因為每個纖維的大小都是 k!（S11），而這依賴物件相異。若物件不可區分，例如字母 A、A、B 排成三個位置，不同的結果只有 AAB、ABA、BAA 三種，不是 3!=6；把 3! 當成排列數就多算了一倍。這類情況需要另外的計數模型（MKO para2）。

0!=1 與空選取k=0 時有序與無序選取都只有一種：空元組與空集合（S03、S14）。若把 0! 誤當 0，C(n,0)=n!/(0!·n!) 會變成除以零；若認為「什麼都不選不算一種」，C(5,0) 會被誤算成 0。


- 從 {a,b,c,d,e} 中可重複地組成三位字母密碼，共有 P(5,3)=60 種 → reject — 可重複時每位都有 5 種，共 5³=125；P(5,3) 只計各項兩兩相異的有序選取。
- 從 5 人中選出會長與秘書（兩個不同職位）的方法數是 C(5,2)=10 → reject — 職位區分順序：甲任會長、乙任秘書與乙任會長、甲任秘書不同，應為 P(5,2)=20=10·2!。
- 字母 A、A、B 的不同排列共有 3!=6 種 → reject — 物件不相異，實際只有 AAB、ABA、BAA 三種；這超出本 MKO 的相異物件模型。
- C(5,0)=0，因為什麼都沒有選 → reject — 空選取計為一種：5!/(0!·5!)=1，且 𝒞_0(X)={∅}。





## 結論與限制

對 n 個相異物件、0≤k≤n、無放回不重複的選取：有序選取數 P(n,k)=n!/(n−k)!（第 i 次可選 n−i+1 個，S06 至 S08），無序選取數 C(n,k)=n!/(k!(n−k)!)（每個 k 元子集合恰有 k! 種排序，S11 至 S13），k=0 時兩者都是 1。例：P(5,3)=60，C(5,3)=10。


- disjoint_union_count 是 finite_counting_basics 兩集合情形對集合個數的歸納推廣，本稿把它當作前置規則，沒有寫出該歸納。
- N11、N12 只是 n 從 3 到 25 的有限點核對，用來交叉檢查公式的寫法；一般結論依賴 S08 與 S13 的證明，不依賴這些核對。
- 可重複選取、不可區分物件與環形排列的計數不在本稿範圍；負面對照中的數字只用來說明公式不適用。





## 驗證及來源綁定

16 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 87cb2ae2d23efddad0cb4a3c6cf56e3e9661d77e4fa32202b282969bac1604f2
- original source SHA-256: 87cb2ae2d23efddad0cb4a3c6cf56e3e9661d77e4fa32202b282969bac1604f2
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-permutation-combination-01.json)