Step
*
1
of Lemma
rv-extend-1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. r0 < d(a;b)
5. s : {s:ℝ| r0 ≤ s}
⊢ ∃x:ℝ^n. ((d(b;x) = s) ∧ ((r0 < s)
⇒ a-b-x))
BY
{ (D 0 With ⌜(d(a;b) + s/d(a;b))*b + (-(s)/d(a;b))*a⌝ THEN Auto) }
1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. r0 < d(a;b)
5. s : {s:ℝ| r0 ≤ s}
⊢ d(b;(d(a;b) + s/d(a;b))*b + (-(s)/d(a;b))*a) = s
2
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. r0 < d(a;b)
5. s : {s:ℝ| r0 ≤ s}
6. d(b;(d(a;b) + s/d(a;b))*b + (-(s)/d(a;b))*a) = s
7. r0 < s
⊢ a-b-(d(a;b) + s/d(a;b))*b + (-(s)/d(a;b))*a
Latex:
Latex:
1. n : \mBbbN{}
2. a : \mBbbR{}\^{}n
3. b : \mBbbR{}\^{}n
4. r0 < d(a;b)
5. s : \{s:\mBbbR{}| r0 \mleq{} s\}
\mvdash{} \mexists{}x:\mBbbR{}\^{}n. ((d(b;x) = s) \mwedge{} ((r0 < s) {}\mRightarrow{} a-b-x))
By
Latex:
(D 0 With \mkleeneopen{}(d(a;b) + s/d(a;b))*b + (-(s)/d(a;b))*a\mkleeneclose{} THEN Auto)
Home
Index