Nuprl Definition : rat-interval-dimension
dim(I) ==  let a,b = I in if q_less(a;b) then 1 else 0 fi 
Definitions occuring in Statement : 
q_less: q_less(r;s)
, 
ifthenelse: if b then t else f fi 
, 
spread: spread def, 
natural_number: $n
Definitions occuring in definition : 
natural_number: $n
, 
q_less: q_less(r;s)
, 
ifthenelse: if b then t else f fi 
, 
spread: spread def
FDL editor aliases : 
ri-dim
ri-dim
Latex:
dim(I)  ==    let  a,b  =  I  in  if  q\_less(a;b)  then  1  else  0  fi 
Date html generated:
2019_10_29-AM-07_47_49
Last ObjectModification:
2019_10_17-PM-03_26_43
Theory : rationals
Home
Index