---

Step * 1 of Lemma r2-plane-separation

.....set predicate..... 
1. a : ℝ^2
2. b : ℝ^2
3. u : {u:ℝ^2| r2-left(u;a;b)} 
4. v : {v:ℝ^2| r2-left(v;b;a)} 
5. x : ℝ^2
6. (¬((¬a_b_x) ∧ (¬b_x_a) ∧ (¬x_a_b))) ∧ u_x_v
⊢ (¬(r2-left(a;b;x) ∨ r2-left(a;x;b)))
∧ ((¬(d(u;v) < d(u;x))) ∧ (¬(d(u;v) < d(x;v))))
∧ (¬(r2-left(u;x;v) ∨ r2-left(u;v;x)))
BY
{ ParallelLast }

1
1. a : ℝ^2
2. b : ℝ^2
3. u : {u:ℝ^2| r2-left(u;a;b)} 
4. v : {v:ℝ^2| r2-left(v;b;a)} 
5. x : ℝ^2
6. u_x_v
7. ¬((¬a_b_x) ∧ (¬b_x_a) ∧ (¬x_a_b))
⊢ ¬(r2-left(a;b;x) ∨ r2-left(a;x;b))

2
1. a : ℝ^2
2. b : ℝ^2
3. u : {u:ℝ^2| r2-left(u;a;b)} 
4. v : {v:ℝ^2| r2-left(v;b;a)} 
5. x : ℝ^2
6. ¬((¬a_b_x) ∧ (¬b_x_a) ∧ (¬x_a_b))
7. u_x_v
⊢ ((¬(d(u;v) < d(u;x))) ∧ (¬(d(u;v) < d(x;v)))) ∧ (¬(r2-left(u;x;v) ∨ r2-left(u;v;x)))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  u  :  \{u:\mBbbR{}\^{}2|  r2-left(u;a;b)\} 
4.  v  :  \{v:\mBbbR{}\^{}2|  r2-left(v;b;a)\} 
5.  x  :  \mBbbR{}\^{}2
6.  (\mneg{}((\mneg{}a\_b\_x)  \mwedge{}  (\mneg{}b\_x\_a)  \mwedge{}  (\mneg{}x\_a\_b)))  \mwedge{}  u\_x\_v
\mvdash{}  (\mneg{}(r2-left(a;b;x)  \mvee{}  r2-left(a;x;b)))
\mwedge{}  ((\mneg{}(d(u;v)  <  d(u;x)))  \mwedge{}  (\mneg{}(d(u;v)  <  d(x;v))))
\mwedge{}  (\mneg{}(r2-left(u;x;v)  \mvee{}  r2-left(u;v;x)))


By

---

Latex:
ParallelLast

---

Home Index