---

Step * 1 of Lemma mon_itop_txpose_invar


1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
4. x : ℕ+n
⊢ (Π 0 ≤ j < n. E[swap(x;0) j]) = (Π 0 ≤ j < n. E[j]) ∈ |g|
BY
{ (% Need typed swap for this to work... %
RWH (FoldWithC [n] `tswap`) 0) }

1
1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
4. x : ℕ+n
⊢ (Π 0 ≤ j < n. E[swap{n}(x;0) j]) = (Π 0 ≤ j < n. E[j]) ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  n  :  \mBbbN{}
3.  E  :  \mBbbN{}n  {}\mrightarrow{}  |g|
4.  x  :  \mBbbN{}\msupplus{}n
\mvdash{}  (\mPi{}  0  \mleq{}  j  <  n.  E[swap(x;0)  j])  =  (\mPi{}  0  \mleq{}  j  <  n.  E[j])


By

---

Latex:
(\%  Need  typed  swap  for  this  to  work...  \%
RWH  (FoldWithC  [n]  `tswap`)  0)

---

Home Index