---

Step * 1 of Lemma sym_grp_is_swaps_a


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))
BY
{ (InstLemma `sym_grp_is_swaps` [n; p] THENA Auto) }

1
1. n : {1...}
2. p : Sym(n)
3. ∃abs:(ℕn × ℕn) List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ 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:

1.  n  :  \{1...\}
2.  p  :  Sym(n)
\mvdash{}  \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:
(InstLemma  `sym\_grp\_is\_swaps`  [n;  p]  THENA  Auto)

---

Home Index