---

Step * 1 2 of Lemma r2-left-separated


1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. d : ℝ^2
5. r0 < |acd|
6. r0 < |bdc|
7. r0 < (|acd| + |bdc|)
8. (|acd| + |bdc|) = a - b⋅λi.if (i =z 0) then (c 1) - d 1 else (d 0) - c 0 fi 
⊢ r0 < ||a - b||
BY
{ ((RWO  "-1" (-2) THENA Auto)
   THEN MoveToConcl (-2)
   THEN (GenConcl ⌜(λi.if (i =z 0) then (c 1) - d 1 else (d 0) - c 0 fi ) = z ∈ ℝ^2⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. a : ℝ^2
2. b : ℝ^2
3. z : ℝ^2
⊢ (r0 < a - b⋅z) ⇒ (r0 < ||a - b||)

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  c  :  \mBbbR{}\^{}2
4.  d  :  \mBbbR{}\^{}2
5.  r0  <  |acd|
6.  r0  <  |bdc|
7.  r0  <  (|acd|  +  |bdc|)
8.  (|acd|  +  |bdc|)  =  a  -  b\mcdot{}\mlambda{}i.if  (i  =\msubz{}  0)  then  (c  1)  -  d  1  else  (d  0)  -  c  0  fi 
\mvdash{}  r0  <  ||a  -  b||


By

---

Latex:
((RWO    "-1"  (-2)  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}i.if  (i  =\msubz{}  0)  then  (c  1)  -  d  1  else  (d  0)  -  c  0  fi  )  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index