---

Step * 1 of Lemma sym_grp_is_swaps


1. p : Sym(0)
⊢ ∃abs:(ℕ0 × ℕ0) List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(0))
BY
{ (With [] (D 0) THENA Auto) }

1
1. p : Sym(0)
⊢ p = (Π map(λab.let a,b = ab in txpose_perm(a;b);[])) ∈ Sym(0)

---

Latex:

---

Latex:

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


By

---

Latex:
(With  []  (D  0)  THENA  Auto)

---

Home Index