---

Step * 1 of Lemma proj-permute_wf


1. n : ℕ
2. p : ℝ^n + 1
3. ∃k:ℕn + 1. p k ≠ r0
4. f : ℕn + 1 ⟶ ℕn + 1
5. Surj(ℕn + 1;ℕn + 1;f)
⊢ proj-permute(p;f) ∈ ℝ^n + 1
BY
{ ProveWfLemma }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  p  :  \mBbbR{}\^{}n  +  1
3.  \mexists{}k:\mBbbN{}n  +  1.  p  k  \mneq{}  r0
4.  f  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbN{}n  +  1
5.  Surj(\mBbbN{}n  +  1;\mBbbN{}n  +  1;f)
\mvdash{}  proj-permute(p;f)  \mmember{}  \mBbbR{}\^{}n  +  1


By

---

Latex:
ProveWfLemma

---

Home Index