---

Step * 1 1 of Lemma sym_grp_is_swaps_a


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))
BY
{ D 3 }

1
1. n : {1...}
2. p : Sym(n)
3. abs : (ℕn × ℕn) List
4. 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)
3.  \mexists{}abs:(\mBbbN{}n  \mtimes{}  \mBbbN{}n)  List.  (p  =  (\mPi{}  map(\mlambda{}ab.let  a,b  =  ab  in  txpose\_perm(a;b);abs)))
\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:
D  3

---

Home Index