Nuprl Definition : prod-ss

ss1 × ss2 ==
  Point=Point × Point
  #=λp,q. (fst(p) # fst(q) ∨ snd(p) # snd(q))
  symm=λx,y,d. case d
               of inl(a) =>
               inl (ss1."#symm" (fst(x)) (fst(y)) a)
               | inr(b) =>
               inr (ss2."#symm" (snd(x)) (snd(y)) b) 
  cotrans=λx,y,z,d. case d
                    of inl(a) =>
                    case ss1."#or" (fst(x)) (fst(y)) (fst(z)) a of inl(u) => inl inl u | inr(u) => inr (inl u) 
                    | inr(b) =>
                    case ss2."#or" (snd(x)) (snd(y)) (snd(z)) b of inl(u) => inl (inr u ) | inr(u) => inr inr u  


Definitions occuring in Statement :  mk-ss: mk-ss,  ss-sep: x # y,  ss-point: Point,  pi1: fst(t),  pi2: snd(t),  or: P ∨ Q,  apply: f a,  lambda: λx.A[x],  product: x:A × B[x],  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 :  inr: inr x ,  inl: inl x,  pi2: snd(t),  token: "$token",  record-select: r.x,  apply: f a,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  pi1: fst(t),  lambda: λx.A[x],  ss-sep: x # y,  or: P ∨ Q,  ss-point: Point,  product: x:A × B[x],  mk-ss: mk-ss
FDL editor aliases :  prod-ss
Latex:
ss1  \mtimes{}  ss2  ==
    Point=Point  \mtimes{}  Point
    \#=\mlambda{}p,q.  (fst(p)  \#  fst(q)  \mvee{}  snd(p)  \#  snd(q))
    symm=\mlambda{}x,y,d.  case  d
                              of  inl(a)  =>
                              inl  (ss1."\#symm"  (fst(x))  (fst(y))  a)
                              |  inr(b)  =>
                              inr  (ss2."\#symm"  (snd(x))  (snd(y))  b) 
    cotrans=\mlambda{}x,y,z,d.  case  d
                                        of  inl(a)  =>
                                        case  ss1."\#or"  (fst(x))  (fst(y))  (fst(z))  a
                                          of  inl(u)  =>
                                          inl  inl  u
                                          |  inr(u)  =>
                                          inr  (inl  u) 
                                        |  inr(b)  =>
                                        case  ss2."\#or"  (snd(x))  (snd(y))  (snd(z))  b
                                          of  inl(u)  =>
                                          inl  (inr  u  )
                                          |  inr(u)  =>
                                          inr  inr  u   


Date html generated: 2016_11_08-AM-09_11_58
Last ObjectModification: 2016_11_02-AM-11_35_26

Theory : inner!product!spaces


Home Index