---

Step * of Lemma r2-left-convex

∀a,b,x,y,z:ℝ^2.  (r2-left(x;a;b) ⇒ r2-left(z;a;b) ⇒ rv-T(2;x;y;z) ⇒ r2-left(y;a;b))
BY
{ (Unfold `r2-left` 0
   THEN Auto
   THEN (Assert ⌜rmin(|xab|;|zab|) ≤ |yab|⌝⋅ THENM (RWO  "-1<" 0 THEN EAuto 1))
   THEN StableCases ⌜x ≠ y⌝⋅
   THEN Try (BLemma `stable__rleq`)
   THEN Auto) }

1
1. a : ℝ^2
2. b : ℝ^2
3. x : ℝ^2
4. y : ℝ^2
5. z : ℝ^2
6. r0 < |xab|
7. r0 < |zab|
8. rv-T(2;x;y;z)
9. x ≠ y
⊢ rmin(|xab|;|zab|) ≤ |yab|

2
1. a : ℝ^2
2. b : ℝ^2
3. x : ℝ^2
4. y : ℝ^2
5. z : ℝ^2
6. r0 < |xab|
7. r0 < |zab|
8. rv-T(2;x;y;z)
9. ¬x ≠ y
⊢ rmin(|xab|;|zab|) ≤ |yab|

---

Latex:

---

Latex:
\mforall{}a,b,x,y,z:\mBbbR{}\^{}2.    (r2-left(x;a;b)  {}\mRightarrow{}  r2-left(z;a;b)  {}\mRightarrow{}  rv-T(2;x;y;z)  {}\mRightarrow{}  r2-left(y;a;b))


By

---

Latex:
(Unfold  `r2-left`  0
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}rmin(|xab|;|zab|)  \mleq{}  |yab|\mkleeneclose{}\mcdot{}  THENM  (RWO    "-1<"  0  THEN  EAuto  1))
  THEN  StableCases  \mkleeneopen{}x  \mneq{}  y\mkleeneclose{}\mcdot{}
  THEN  Try  (BLemma  `stable\_\_rleq`)
  THEN  Auto)

---

Home Index