Step
*
2
1
1
of Lemma
sym_grp_is_swaps
1. n : ℤ
2. [%1] : 0 < n
3. p : Sym(n)
4. q : Sym(n - 1)
5. i : ℕn
6. j : ℕn
7. p = txpose_perm(i;j) O ↑{n - 1}(q) ∈ Sym(n)
8. abs : (ℕn - 1 × ℕn - 1) List
9. q = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(n - 1)
⊢ ∃abs:(ℕn × ℕn) List. (p = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(n))
BY
{ (With [<i, j> / abs] (D 0) THENA Auto) }
1
1. n : ℤ
2. 0 < n
3. p : Sym(n)
4. q : Sym(n - 1)
5. i : ℕn
6. j : ℕn
7. p = txpose_perm(i;j) O ↑{n - 1}(q) ∈ Sym(n)
8. abs : (ℕn - 1 × ℕn - 1) List
9. q = (Π map(λab.let a,b = ab in txpose_perm(a;b);abs)) ∈ Sym(n - 1)
⊢ p = (Π map(λab.let a,b = ab in txpose_perm(a;b);[<i, j> / abs])) ∈ Sym(n)
Latex:
Latex:
1. n : \mBbbZ{}
2. [\%1] : 0 < n
3. p : Sym(n)
4. q : Sym(n - 1)
5. i : \mBbbN{}n
6. j : \mBbbN{}n
7. p = txpose\_perm(i;j) O \muparrow{}\{n - 1\}(q)
8. abs : (\mBbbN{}n - 1 \mtimes{} \mBbbN{}n - 1) List
9. q = (\mPi{} map(\mlambda{}ab.let a,b = ab in txpose\_perm(a;b);abs))
\mvdash{} \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:
(With [<i, j> / abs] (D 0) THENA Auto)
Home
Index