Nuprl Definition : rv-orthog-ext

rv-orthog-ext(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


Definitions occuring in Statement :  rv-norm: ||x||,  rv-sub: x - y,  rv-minus: -x,  rv-add: x + y,  rv-0: 0,  rlessw: rlessw(x;y),  rnexp: x^k1,  int-to-real: r(n),  apply: f a,  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  multiply: n * m,  add: n + m,  natural_number: $n,  token: "$token",  axiom: Ax,  record-select: r.x
Definitions occuring in definition :  axiom: Ax,  rv-minus: -x,  rv-add: x + y,  rv-0: 0,  token: "$token",  record-select: r.x,  apply: f a,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  natural_number: $n,  rv-sub: x - y,  rv-norm: ||x||,  rnexp: x^k1,  int-to-real: r(n),  rlessw: rlessw(x;y),  multiply: n * m,  add: n + m,  spread: spread def,  lambda: λx.A[x]
FDL editor aliases :  rv-orthog-ext
Latex:
rv-orthog-ext(rv;f)  ==
    \mlambda{}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


Date html generated: 2016_11_08-AM-09_18_37
Last ObjectModification: 2016_11_02-PM-04_22_32

Theory : inner!product!spaces


Home Index