DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  i=j == if i=j true ; false fi

is mentioned by

Thm*  f:(a bij a). InvFuns(a;a;f;y.least x:f(x)=y)[nsub_bij_least_preimage_inverse]
Thm*  f:(a onto b). (y.least x:f(x)=y b inj a[nsub_surj_imp_a_rev_inj]
Thm*  (A+B) ~ (i:2if i=0 A else B fi)[card_union_vs_sigma]
Thm*  InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union)[union_sigma_inverses]
Thm*  A,B:Type. sigma_to_union  (i:2if i=0 A else B fi)(A+B)[sigma_to_union_wf]
Thm*  A,B:Type. union_to_sigma  (A+B)(i:2if i=0 A else B fi)[union_to_sigma_wf]
Thm*  Dec(P (!i:2. if i=0 P else P fi)[decidable_vs_unique_nsub2]
Thm*  f:(a onto b), y:bf(least x:f(x)=y) = y[nsub_surj_least_preimage_works]
Thm*  f:(a onto b), y:b. (least x:f(x)=y a[nsub_surj_least_preimage_total]
Thm*  a:b:j:bf:((a-1) inj {x:bx = j }).
Thm*  (i.if i=a-1 j else f(i) fi)  a inj b
Thm*  IsEqFun(b;i,ji=j)[eq_int_is_eq_nsub]
Def  prev_nat_pair(xy) == xy/x,y. if x=0 <y-1,0> else <x-1,y+1> fi[prev_nat_pair]
Def  next_nat_pair(xy) == xy/x,y. if y=0 <0,x+1> else <x+1,y-1> fi[next_nat_pair]
Def  [xxs](i) == if i=0 x else xs(i-1) fi[seq_cons]
Def  sigma_to_union(e) == e/i,u. if i=0 inl(u) else inr(u) fi[sigma_to_union]
Def  f{i}(x) == if i=0 x else f(f{i-1}(x)) fi  (recursive)[compose_iter]
Def  Replace value k by f(m) in f == Replace values x s.t. x=k by f(m) in f[delete_fenum_value]

In prior sections: bool 1 LogicSupplement int 2 num thy 1

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

DiscreteMath Sections DiscrMathExt Doc