Step
*
2
of Lemma
real-vec-sep-0-iff
1. n : ℕ
2. x : ℝ^n
3. r0 < x⋅x
4. req-vec(n;x - λi.r0;x)
⊢ r0 < ||x - λi.r0||
BY
{ ((RWO "-1" 0 THENA Auto) THEN Thin (-1)) }
1
1. n : ℕ
2. x : ℝ^n
3. r0 < x⋅x
⊢ r0 < ||x||
Latex:
Latex:
1. n : \mBbbN{}
2. x : \mBbbR{}\^{}n
3. r0 < x\mcdot{}x
4. req-vec(n;x - \mlambda{}i.r0;x)
\mvdash{} r0 < ||x - \mlambda{}i.r0||
By
Latex:
((RWO "-1" 0 THENA Auto) THEN Thin (-1))
Home
Index