---

Step * 2 1 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 ↑{n}(Π v) ∈ Sym(n + 1)
BY
{ TACTIC:(BackThruLemma `extend_perm_over_comp` THEN Auto) }

---

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  \muparrow{}\{n\}(\mPi{}  v)


By

---

Latex:
TACTIC:(BackThruLemma  `extend\_perm\_over\_comp`  THEN  Auto)

---

Home Index