---

Step * of Lemma rv-norm-positive-iff-ext

∀rv:InnerProductSpace. ∀x:Point.  (x # 0 ⇐⇒ r0 < ||x||)
BY
{ Extract of Obid: rv-norm-positive-iff
  normalizes to:
  
  λrv,x. <λ%.rlessw(r0;rsqrt(rv."ip" x x))
         , λ%.let %16,%17 = rv."positive" x 
              in %17 ((((rlessw(r0^2;||x||^2) * 20) + 1) * 20) + 1)
         >
  
  not unfolding  rsqrt rlessw rnexp rv-norm rmul int-to-real record-select
  finishing with (Reduce 0
                  THEN (Assert ∀x,rv:Top.
                                 (TERMOF{rnexp-rless:o, \\v:l} r0 ||x|| TERMOF{rleq_weakening_equal:o, \\v:l} 
                                 ~ λ%1,n. rlessw(r0^n;||x||^n)) BY
                              (Auto THEN RW (AddrC [1] (TagC (mk_tag_term 10))) 0 THEN Auto))
                  THEN (RWO  "-1" 0 THEN Reduce 0)
                  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}x:Point.    (x  \#  0  \mLeftarrow{}{}\mRightarrow{}  r0  <  ||x||)


By

---

Latex:
Extract  of  Obid:  rv-norm-positive-iff
normalizes  to:

\mlambda{}rv,x.  <\mlambda{}\%.rlessw(r0;rsqrt(rv."ip"  x  x))
              ,  \mlambda{}\%.let  \%16,\%17  =  rv."positive"  x 
                        in  \%17  ((((rlessw(r0\^{}2;||x||\^{}2)  *  20)  +  1)  *  20)  +  1)
              >

not  unfolding    rsqrt  rlessw  rnexp  rv-norm  rmul  int-to-real  record-select
finishing  with  (Reduce  0
                                THEN  (Assert  \mforall{}x,rv:Top.
                                                              (TERMOF\{rnexp-rless:o,  \mbackslash{}\mbackslash{}v:l\}  r0  ||x|| 
                                                                TERMOF\{rleq\_weakening\_equal:o,  \mbackslash{}\mbackslash{}v:l\}  \msim{}  \mlambda{}\%1,n.  rlessw(r0\^{}n;||x||\^{}n))\000C  BY
                                                        (Auto  THEN  RW  (AddrC  [1]  (TagC  (mk\_tag\_term  10)))  0  THEN  Auto))
                                THEN  (RWO    "-1"  0  THEN  Reduce  0)
                                THEN  Auto)

---

Home Index