Nuprl Definition : permutation-s-group

Perm(rv) ==
  mk-s-group(permutation-ss(rv);
             <λx.x, λx.x>;
             λfg.let f,g = fg 
                 in <g, f>;
             λfg,fg'. let f,g = fg in let f',g' = fg' in <f o f', g' o g>;
             λx,y,z,w,d. case d
                         of inl(asep) =>
                         let a,sep = asep 
                         in inl inl <(fst(z)) a, sep>
                         | inr(asep) =>
                         let a,sep = asep 
                         in inl (inr <a, sepw ((snd(x)) a) ((snd(y)) a)> );
             λx,y,d. case d of inl(asep) => inr asep  | inr(asep) => inl asep)


Definitions occuring in Statement :  permutation-ss: permutation-ss(ss),  mk-s-group: mk-s-group(ss; e; i; o; sep; invsep),  compose: f o g,  pi1: fst(t),  pi2: snd(t),  apply: f a,  lambda: λx.A[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
Definitions occuring in definition :  inl: inl x,  inr: inr x ,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  lambda: λx.A[x],  pi2: snd(t),  apply: f a,  pair: <a, b>,  spread: spread def,  pi1: fst(t),  compose: f o g,  permutation-ss: permutation-ss(ss),  mk-s-group: mk-s-group(ss; e; i; o; sep; invsep)
FDL editor aliases :  permutation-s-group
Latex:
Perm(rv)  ==
    mk-s-group(permutation-ss(rv);
                          <\mlambda{}x.x,  \mlambda{}x.x>
                          \mlambda{}fg.let  f,g  =  fg 
                                  in  <g,  f>
                          \mlambda{}fg,fg'.  let  f,g  =  fg  in  let  f',g'  =  fg'  in  <f  o  f',  g'  o  g>
                          \mlambda{}x,y,z,w,d.  case  d
                                                  of  inl(asep)  =>
                                                  let  a,sep  =  asep 
                                                  in  inl  inl  <(fst(z))  a,  sep>
                                                  |  inr(asep)  =>
                                                  let  a,sep  =  asep 
                                                  in  inl  (inr  <a,  sepw  ((snd(x))  a)  ((snd(y))  a)>  );
                          \mlambda{}x,y,d.  case  d  of  inl(asep)  =>  inr  asep    |  inr(asep)  =>  inl  asep)


Date html generated: 2016_11_08-AM-09_12_51
Last ObjectModification: 2016_11_03-AM-11_03_47

Theory : inner!product!spaces


Home Index