---

Step * 2 of Lemma extend_perm_over_itcomp


1. n : ℕ
2. u : Sym(n)
3. v : Sym(n) List
4. ↑{n}(Π v) = (Π map(λp.↑{n}(p);v)) ∈ Sym(n + 1)
⊢ ↑{n}(Π [u / v]) = (Π map(λp.↑{n}(p);[u / v])) ∈ Sym(n + 1)
BY
{ AbReduce 0 }

1
1. n : ℕ
2. u : Sym(n)
3. v : Sym(n) List
4. ↑{n}(Π v) = (Π map(λp.↑{n}(p);v)) ∈ Sym(n + 1)
⊢ ↑{n}(u O (Π v)) = ↑{n}(u) O (Π map(λp.↑{n}(p);v)) ∈ Sym(n + 1)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  u  :  Sym(n)
3.  v  :  Sym(n)  List
4.  \muparrow{}\{n\}(\mPi{}  v)  =  (\mPi{}  map(\mlambda{}p.\muparrow{}\{n\}(p);v))
\mvdash{}  \muparrow{}\{n\}(\mPi{}  [u  /  v])  =  (\mPi{}  map(\mlambda{}p.\muparrow{}\{n\}(p);[u  /  v]))


By

---

Latex:
AbReduce  0

---

Home Index