---

Step * 1 2 1 of Lemma extend_perm_over_comp


1. n : ℕ
2. p : Sym(n)
3. q : Sym(n)
4. ↑{n}(p
         O q) ∈ Sym(n + 1)
⊢ InvFuns(ℕn + 1;ℕn + 1;↑{n}(p
                              O q).f;↑{n}(p
                                           O q).b)
BY
{ ((Unfold `sym_grp` 4 THEN AddProperties 4) THEN Auto{1,3}-1) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  p  :  Sym(n)
3.  q  :  Sym(n)
4.  \muparrow{}\{n\}(p
                  O  q)  \mmember{}  Sym(n  +  1)
\mvdash{}  InvFuns(\mBbbN{}n  +  1;\mBbbN{}n  +  1;\muparrow{}\{n\}(p
                                                            O  q).f;\muparrow{}\{n\}(p
                                                                                      O  q).b)


By

---

Latex:
((Unfold  `sym\_grp`  4  THEN  AddProperties  4)  THEN  Auto\{1,3\}-1)

---

Home Index