Nuprl Definition : fun-ss

A ⟶ ss ==
  Point=A ⟶ Point
  #=λf,g. fun-sep(ss;A;f;g)
  symm=λf,g,fsep. let a,sep = fsep in <a, ss."#symm" (f a) (g a) sep>
  cotrans=λf,g,h,fsep. let a,sep = fsep 
                       in case ss."#or" (f a) (g a) (h a) sep of inl(x) => inl <a, x> | inr(y) => inr <a, y> 


Definitions occuring in Statement :  fun-sep: fun-sep(ss;A;f;g),  mk-ss: mk-ss,  ss-point: Point,  apply: f a,  lambda: λx.A[x],  function: x:A ⟶ B[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  token: "$token",  record-select: r.x
Definitions occuring in definition :  pair: <a, b>,  inr: inr x ,  inl: inl x,  apply: f a,  token: "$token",  record-select: r.x,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  lambda: λx.A[x],  fun-sep: fun-sep(ss;A;f;g),  ss-point: Point,  function: x:A ⟶ B[x],  mk-ss: mk-ss
FDL editor aliases :  fun-ss
Latex:
A  {}\mrightarrow{}  ss  ==
    Point=A  {}\mrightarrow{}  Point
    \#=\mlambda{}f,g.  fun-sep(ss;A;f;g)
    symm=\mlambda{}f,g,fsep.  let  a,sep  =  fsep  in  <a,  ss."\#symm"  (f  a)  (g  a)  sep>
    cotrans=\mlambda{}f,g,h,fsep.  let  a,sep  =  fsep 
                                              in  case  ss."\#or"  (f  a)  (g  a)  (h  a)  sep
                                                      of  inl(x)  =>
                                                      inl  <a,  x>
                                                      |  inr(y)  =>
                                                      inr  <a,  y> 


Date html generated: 2016_11_08-AM-09_11_54
Last ObjectModification: 2016_11_02-AM-10_54_58

Theory : inner!product!spaces


Home Index