Step
*
1
2
1
1
1
1
1
of Lemma
ip-between-iff
1. rv : InnerProductSpace
2. t : ℝ
3. v : Point
4. r0 < ||v||
5. ((||v|| * |t| * ||v||) + (t * ||v||^2)) = r0
⊢ t ≤ r0
BY
{ nRNorm (-1) }
1
1. rv : InnerProductSpace
2. t : ℝ
3. v : Point
4. r0 < ||v||
5. ((|t| * ||v|| * ||v||) + (||v||^2 * t)) = r0
⊢ t ≤ r0
Latex:
Latex:
1.  rv  :  InnerProductSpace
2.  t  :  \mBbbR{}
3.  v  :  Point
4.  r0  <  ||v||
5.  ((||v||  *  |t|  *  ||v||)  +  (t  *  ||v||\^{}2))  =  r0
\mvdash{}  t  \mleq{}  r0
By
Latex:
nRNorm  (-1)
Home
Index