---

Step * of Lemma sym_grp_is_swaps

∀n:ℕ. ∀p:Sym(n).  ∃abs:(ℕn × ℕn) List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(n))
BY
{ ((D 0 THENM NatInd (-1)) THEN Auto) }

1
1. p : Sym(0)
⊢ ∃abs:(ℕ0 × ℕ0) List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(0))

2
1. n : ℤ
2. [%1] : 0 < n
3. ∀p:Sym(n - 1). ∃abs:(ℕn - 1 × ℕn - 1) List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(n - 1))
4. p : Sym(n)
⊢ ∃abs:(ℕn × ℕn) List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(n))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}p:Sym(n).    \mexists{}abs:(\mBbbN{}n  \mtimes{}  \mBbbN{}n)  List.  (p  =  (\mPi{}  map(\mlambda{}ab.let  a,b  =  ab  in  txpose\_perm(a;b);abs)))


By

---

Latex:
((D  0  THENM  NatInd  (-1))  THEN  Auto)

---

Home Index