---

Step * 1 of Lemma extend_perm_over_comp


1. n : ℕ
2. p : Sym(n)
3. q : Sym(n)
⊢ ↑{n}(p O q) = ↑{n}(p) O ↑{n}(q) ∈ Sym(n + 1)
BY
{ (EqTypeCD THENW Auto) }

1
1. n : ℕ
2. p : Sym(n)
3. q : Sym(n)
⊢ ↑{n}(p O q) = ↑{n}(p) O ↑{n}(q) ∈ perm_sig(ℕn + 1)

2
.....set predicate..... 
1. n : ℕ
2. p : Sym(n)
3. q : Sym(n)
⊢ InvFuns(ℕn + 1;ℕn + 1;↑{n}(p
                              O q).f;↑{n}(p
                                           O q).b)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  p  :  Sym(n)
3.  q  :  Sym(n)
\mvdash{}  \muparrow{}\{n\}(p  O  q)  =  \muparrow{}\{n\}(p)  O  \muparrow{}\{n\}(q)


By

---

Latex:
(EqTypeCD  THENW  Auto)

---

Home Index