---

Step * 1 of Lemma mon_itop_perm_invar


1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
⊢ ∀p:Sym(n). ((Π 0 ≤ j < n. E[p.f j]) = (Π 0 ≤ j < n. E[j]) ∈ |g|)
BY
{ (Unfold `so_apply` 0 THEN ((BLemma `perm_induction_b` THENM UnivCD) THENA Auto)) }

1
1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
⊢ (Π 0 ≤ j < n. E (id_perm().f j)) = (Π 0 ≤ j < n. E j) ∈ |g|

2
1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
4. p : Sym(n)
5. (Π 0 ≤ j < n. E (p.f j)) = (Π 0 ≤ j < n. E j) ∈ |g|
6. i : ℕ+n
⊢ (Π 0 ≤ j < n. E (p O txpose_perm(i;0).f j)) = (Π 0 ≤ j < n. E j) ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  n  :  \mBbbN{}
3.  E  :  \mBbbN{}n  {}\mrightarrow{}  |g|
\mvdash{}  \mforall{}p:Sym(n).  ((\mPi{}  0  \mleq{}  j  <  n.  E[p.f  j])  =  (\mPi{}  0  \mleq{}  j  <  n.  E[j]))


By

---

Latex:
(Unfold  `so\_apply`  0  THEN  ((BLemma  `perm\_induction\_b`  THENM  UnivCD)  THENA  Auto))

---

Home Index