---

Step * 2 1 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 O (Π v)) = ↑{n}(u) O (Π map(λp.↑{n}(p);v)) ∈ Sym(n + 1)
BY
{ (RevHypSubst (-1) 0 THENA Auto) }

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 ↑{n}(Π 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\}(u  O  (\mPi{}  v))  =  \muparrow{}\{n\}(u)  O  (\mPi{}  map(\mlambda{}p.\muparrow{}\{n\}(p);v))


By

---

Latex:
(RevHypSubst  (-1)  0  THENA  Auto)

---

Home Index