---

Step * 1 1 of Lemma extend_perm_wf


1. n : ℕ
2. p : Perm(ℕn)
⊢ InvFuns(ℕn + 1;ℕn + 1;extend_permf(p.f;n);extend_permf(p.b;n))
BY
{ Unfold `inv_funs` 0 }

1
1. n : ℕ
2. p : Perm(ℕn)
⊢ ((extend_permf(p.b;n) o extend_permf(p.f;n)) = Id{ℕn + 1} ∈ (ℕn + 1 ⟶ ℕn + 1))
∧ ((extend_permf(p.f;n) o extend_permf(p.b;n)) = Id{ℕn + 1} ∈ (ℕn + 1 ⟶ ℕn + 1))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  p  :  Perm(\mBbbN{}n)
\mvdash{}  InvFuns(\mBbbN{}n  +  1;\mBbbN{}n  +  1;extend\_permf(p.f;n);extend\_permf(p.b;n))


By

---

Latex:
Unfold  `inv\_funs`  0

---

Home Index