---

Step * of Lemma proj-sep-or

∀n:ℕ. ∀a,b,c:ℙ^n.  (a ≠ b ⇒ (a ≠ c ∨ b ≠ c))
BY
{ (Auto
   THEN D -1
   THEN (InstLemma `real-vec-sep-cases` [⌜n + 1⌝;⌜u(a)⌝;⌜u(b)⌝]⋅ THENA Auto)
   THEN (InstLemma `real-vec-sep-cases` [⌜n + 1⌝;⌜u(a)⌝;⌜r(-1)*u(b)⌝]⋅ THENA Auto)) }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. c : ℙ^n
5. u(a) ≠ u(b)
6. u(a) ≠ r(-1)*u(b)
7. ∀c:ℝ^n + 1. (u(a) ≠ c ∨ u(b) ≠ c)
8. ∀c:ℝ^n + 1. (u(a) ≠ c ∨ r(-1)*u(b) ≠ c)
⊢ a ≠ c ∨ b ≠ c

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbP{}\^{}n.    (a  \mneq{}  b  {}\mRightarrow{}  (a  \mneq{}  c  \mvee{}  b  \mneq{}  c))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  (InstLemma  `real-vec-sep-cases`  [\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}u(a)\mkleeneclose{};\mkleeneopen{}u(b)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `real-vec-sep-cases`  [\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}u(a)\mkleeneclose{};\mkleeneopen{}r(-1)*u(b)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index