---

Step * of Lemma rv-orthogonal-implies-extensional-ext

No Annotations
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv).  ∀x,y:Point(rv).  (f x # f y ⇒ x # y) supposing Orthogonal(f)
BY
{ Extract of Obid: rv-orthogonal-implies-extensional
  not unfolding  rlessw rsqrt rnexp rv-0 rv-minus rv-sub rv-add rv-norm int-to-real record-select
  finishing with Auto
  normalizes to:
  
  λrv,f,x,y,_. case rv."+sep" -y -y x y 
                    case rv."#or" -y + x 0 -y + x 
                         case rv."#or" x + -y 0 -y + x 
                              let _,h = rv."positive" x - y 
                              in h ((((rlessw(r0^2;||x - y||^2) * 20) + 1) * 20) + 1)
                          of inl(_) =>
                          Ax
                          | inr(a) =>
                          case rv."#or" 0 -y + x 0 a of inl(_) => Ax | inr(x) => x
                     of inl(_) =>
                     Ax
                     | inr(a) =>
                     case rv."#or" 0 -y + x -y + y a of inl(_) => Ax | inr(x) => x
               of inl(_) =>
               Ax
               | inr(x) =>
               x }

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}f:Point(rv)  {}\mrightarrow{}  Point(rv).
    \mforall{}x,y:Point(rv).    (f  x  \#  f  y  {}\mRightarrow{}  x  \#  y)  supposing  Orthogonal(f)


By

---

Latex:
Extract  of  Obid:  rv-orthogonal-implies-extensional
not  unfolding    rlessw  rsqrt  rnexp  rv-0  rv-minus  rv-sub  rv-add  rv-norm  int-to-real  record-select
finishing  with  Auto
normalizes  to:

\mlambda{}rv,f,x,y,$_{}$.  case  rv."+sep"  -y  -y  x  y 
                                  case  rv."\#or"  -y  +  x  0  -y  +  x 
                                            case  rv."\#or"  x  +  -y  0  -y  +  x 
                                                      let  $_{}$,h  =  rv."positive"  x  -  y 
                                                      in  h  ((((rlessw(r0\^{}2;||x  -  y||\^{}2)  *  20)  +  1)  *  20)  +  1)
                                              of  inl($_{}$)  =>
                                              Ax
                                              |  inr(a)  =>
                                              case  rv."\#or"  0  -y  +  x  0  a  of  inl($_{}$)  =>  Ax  |  inr(x)  =\000C>  x
                                    of  inl($_{}$)  =>
                                    Ax
                                    |  inr(a)  =>
                                    case  rv."\#or"  0  -y  +  x  -y  +  y  a  of  inl($_{}$)  =>  Ax  |  inr(x)  =\000C>  x
                        of  inl($_{}$)  =>
                        Ax
                        |  inr(x)  =>
                        x

---

Home Index