---

Step * of Lemma sym_grp_is_swaps_a

∀n:{1...}. ∀p:Sym(n).
  ∃abs:{ab:ℕn × ℕn| fst(ab) < snd(ab)}  List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(n))
BY
{ (UnivCD THENA Auto) }

1
1. n : {1...}
2. p : Sym(n)
⊢ ∃abs:{ab:ℕn × ℕn| fst(ab) < snd(ab)}  List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(n))

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index