---

Step * of Lemma equipollent-factorial

∀n:ℕ. ℕn →⟶ ℕn ~ ℕ(n)!
BY
{ (Auto THEN (RWW "injections-combinations count-combinations" 0 THENA Auto) THEN BLemma `equipollent-nsub` THEN Auto) }

1
1. n : ℕ
⊢ C(n;n) = (n)! ∈ ℤ

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n  \msim{}  \mBbbN{}(n)!


By

---

Latex:
(Auto
  THEN  (RWW  "injections-combinations  count-combinations"  0  THENA  Auto)
  THEN  BLemma  `equipollent-nsub`
  THEN  Auto)

---

Home Index