Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
compose_iterDef  f{i}(x) == if i=0 x else f(f{i-1}(x)) fi  (recursive)
Thm*  f:(AA), i:f{i AA
identityDef  Id(x) == x
Thm*  A:Type. Id  AA
injection_typeDef  A inj B == {f:(AB)| Inj(ABf) }
Thm*  A,B:Type. A inj B  Type
injectDef  Inj(ABf) == a1,a2:Af(a1) = f(a2 B  a1 = a2
Thm*  A,B:Type, f:(AB). Inj(ABf Prop
int_segDef  {i..j} == {k:i  k < j }
Thm*  m,n:. {m..n Type
natDef   == {i:| 0i }
Thm*    Type
nat_plusDef   == {i:| 0<i }
Thm*    Type

About:
ifthenelseintnatural_numbersubtractless_thansetapplyfunction
recursive_def_noticeuniverseequalmemberpropimpliesall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions DiscreteMath Sections DiscrMathExt Doc