---

Step * of Lemma mon_itop_txpose_invar

∀g:IAbMonoid. ∀n:ℕ. ∀E:ℕn ⟶ |g|. ∀x:ℕ+n.  ((Π 0 ≤ j < n. E[txpose_perm(x;0).f j]) = (Π 0 ≤ j < n. E[j]) ∈ |g|)
BY
{ ((UnivCD THENA Auto) THEN AbReduce 0) }

1
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|

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  \mforall{}n:\mBbbN{}.  \mforall{}E:\mBbbN{}n  {}\mrightarrow{}  |g|.  \mforall{}x:\mBbbN{}\msupplus{}n.
    ((\mPi{}  0  \mleq{}  j  <  n.  E[txpose\_perm(x;0).f  j])  =  (\mPi{}  0  \mleq{}  j  <  n.  E[j]))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  AbReduce  0)

---

Home Index