---

Step * of Lemma r2-left-cases

∀a,b:ℝ^2. ∀c:{c:ℝ^2| |a + r(-1)*b⋅c + r(-1)*b| < (||a + r(-1)*b|| * ||c + r(-1)*b||)} .
  (r2-left(a;b;c) ∨ r2-left(a;c;b))
BY
{ (Auto THEN Unfold `r2-left` 0) }

1
1. a : ℝ^2
2. b : ℝ^2
3. c : {c:ℝ^2| |a + r(-1)*b⋅c + r(-1)*b| < (||a + r(-1)*b|| * ||c + r(-1)*b||)} 
⊢ (r0 < |abc|) ∨ (r0 < |acb|)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}\^{}2.  \mforall{}c:\{c:\mBbbR{}\^{}2|  |a  +  r(-1)*b\mcdot{}c  +  r(-1)*b|  <  (||a  +  r(-1)*b||  *  ||c  +  r(-1)*b||)\}  .
    (r2-left(a;b;c)  \mvee{}  r2-left(a;c;b))


By

---

Latex:
(Auto  THEN  Unfold  `r2-left`  0)

---

Home Index