Step
*
of Lemma
real-vec-angle-lemma
∀n:ℕ. ∀x,z:ℝ^n.  (d(z;x) < d(z;r(-1)*x) 
⇐⇒ r0 < x⋅z)
BY
{ (Intros
   THEN RepUR ``real-vec-dist real-vec-norm`` 0
   THEN (RWO "rsqrt-rless-iff<" 0 THENA Auto)
   THEN (RWW "dot-product-linearity1-sub.1 dot-product-linearity1-sub.2" 0⋅ THENA Auto)
   THEN (RWW "dot-product-linearity2.1 dot-product-linearity2.2" 0⋅ THENA Auto)
   THEN (Assert z⋅x = x⋅z BY
               Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN nRNorm 0
   THEN Auto) }
1
1. n : ℕ
2. x : ℝ^n
3. z : ℝ^n
4. z⋅x = x⋅z
5. (x⋅x + (r(-2) * x⋅z) + z⋅z) < (x⋅x + (r(2) * x⋅z) + z⋅z)
⊢ r0 < x⋅z
2
1. n : ℕ
2. x : ℝ^n
3. z : ℝ^n
4. z⋅x = x⋅z
5. r0 < x⋅z
⊢ (x⋅x + (r(-2) * x⋅z) + z⋅z) < (x⋅x + (r(2) * x⋅z) + z⋅z)
Latex:
Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x,z:\mBbbR{}\^{}n.    (d(z;x)  <  d(z;r(-1)*x)  \mLeftarrow{}{}\mRightarrow{}  r0  <  x\mcdot{}z)
By
Latex:
(Intros
  THEN  RepUR  ``real-vec-dist  real-vec-norm``  0
  THEN  (RWO  "rsqrt-rless-iff<"  0  THENA  Auto)
  THEN  (RWW  "dot-product-linearity1-sub.1  dot-product-linearity1-sub.2"  0\mcdot{}  THENA  Auto)
  THEN  (RWW  "dot-product-linearity2.1  dot-product-linearity2.2"  0\mcdot{}  THENA  Auto)
  THEN  (Assert  z\mcdot{}x  =  x\mcdot{}z  BY
                          Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  nRNorm  0
  THEN  Auto)
Home
Index