Nuprl Definition : lower-rc-face
lower-rc-face(c;j) ==  λi.if (i =z j) then [fst((c i))] else c i fi 
Definitions occuring in Statement : 
rat-point-interval: [a]
, 
ifthenelse: if b then t else f fi 
, 
eq_int: (i =z j)
, 
pi1: fst(t)
, 
apply: f a
, 
lambda: λx.A[x]
Definitions occuring in definition : 
apply: f a
, 
pi1: fst(t)
, 
rat-point-interval: [a]
, 
eq_int: (i =z j)
, 
ifthenelse: if b then t else f fi 
, 
lambda: λx.A[x]
FDL editor aliases : 
lower-rc-face
Latex:
lower-rc-face(c;j)  ==    \mlambda{}i.if  (i  =\msubz{}  j)  then  [fst((c  i))]  else  c  i  fi 
Date html generated:
2019_10_29-AM-07_55_55
Last ObjectModification:
2019_10_17-PM-03_00_18
Theory : rationals
Home
Index