---

Step * 1 of Lemma extend_permf_over_swap


1. n : ℕ
2. i : ℕn
3. j : ℕn
⊢ extend_permf(swap(i;j);n) = swap(i;j) ∈ (ℕn + 1 ⟶ ℕn + 1)
BY
{ (ExtWith [`k'] [ℕn + 1 ⟶ ℕn + 1] THENA Auto) }

1
1. n : ℕ
2. i : ℕn
3. j : ℕn
4. k : ℕn + 1
⊢ (extend_permf(swap(i;j);n) k) = (swap(i;j) k) ∈ ℕn + 1

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  j  :  \mBbbN{}n
\mvdash{}  extend\_permf(swap(i;j);n)  =  swap(i;j)


By

---

Latex:
(ExtWith  [`k']  [\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbN{}n  +  1]  THENA  Auto)

---

Home Index