---

Step * 1 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|)
⊢ r0 < ||a - b||
BY
{ Assert ⌜(|acd| + |bdc|) = a - b⋅λi.if (i =z 0) then (c 1) - d 1 else (d 0) - c 0 fi ⌝⋅ }

1
.....assertion..... 
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. d : ℝ^2
5. r0 < |acd|
6. r0 < |bdc|
7. r0 < (|acd| + |bdc|)
⊢ (|acd| + |bdc|) = a - b⋅λi.if (i =z 0) then (c 1) - d 1 else (d 0) - c 0 fi 

2
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||

---

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|)
\mvdash{}  r0  <  ||a  -  b||


By

---

Latex:
Assert  \mkleeneopen{}(|acd|  +  |bdc|)  =  a  -  b\mcdot{}\mlambda{}i.if  (i  =\msubz{}  0)  then  (c  1)  -  d  1  else  (d  0)  -  c  0  fi  \mkleeneclose{}\mcdot{}

---

Home Index