---

Step * of Lemma not-proj-sep

∀n:ℕ. ∀a,b:ℙ^n.  (¬a ≠ b ⇐⇒ req-vec(n + 1;u(a);u(b)) ∨ req-vec(n + 1;u(a);r(-1)*u(b)))
BY
{ Auto }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. ¬a ≠ b
⊢ req-vec(n + 1;u(a);u(b)) ∨ req-vec(n + 1;u(a);r(-1)*u(b))

2
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. req-vec(n + 1;u(a);u(b)) ∨ req-vec(n + 1;u(a);r(-1)*u(b))
⊢ ¬a ≠ b

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbP{}\^{}n.    (\mneg{}a  \mneq{}  b  \mLeftarrow{}{}\mRightarrow{}  req-vec(n  +  1;u(a);u(b))  \mvee{}  req-vec(n  +  1;u(a);r(-1)*u(b)))


By

---

Latex:
Auto

---

Home Index