DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  P & Q == PQ

is mentioned by

Thm*  (A  C)  (B  D)  A & B  C & D[parallel_conjunct_imp]
Thm*  InvFuns(A;B;f;g)  Inj(A; B; f) & Inj(B; A; g)[invfuns_are_inj]
Thm*  InvFuns(A;B;f;g)  Surj(A; B; f) & Surj(B; A; g)[invfuns_are_surj]
Thm*  R:(ABProp). 
Thm*  (1-1-Corr x:A,y:B. R(x;y))
Thm*  
Thm*  (f:(AB), g:(BA).
Thm*  (InvFuns(A;B;f;g) & (x:A, y:B. R(x;y)  y = f(x) & x = g(y)))		[one_one_corr_rel_vs_invfuns]
Thm*  P:{P:(Prop)| i:. P(i) }. 
Thm*  (i:. Dec(P(i)))  ({i:| P(i) & (j:. j<i  P(j)) })		[least_exists2]
Thm*  k:, P:{P:(kProp)| i:k. P(i) }.
Thm*  (i:k. Dec(P(i)))  ({i:k| P(i) & (j:i. P(j)) })		[least_exists]
Thm*  {x:{x:A| P(x) }| Q(x) } ~ {x:A| P(x) & Q(x) }[card_subset_vs_and]
Thm*  (A:Type, R:(AAProp).
Thm*  ((A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y))
Thm*  (& (x:A. R(x;x))
Thm*  (& Finite(A))		[no_finite_model]
Thm*  R:(AAProp). 
Thm*  (A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y))
Thm*  
Thm*  (k:. f:(kA). i,j:k. i<j  R(f(i);f(j)))		[no_finite_model_lemma]
Thm*  p:{p:()| i:. p(i) }. 
Thm*  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }		[least_characterized2]
Thm*  k:, p:{p:(k)| i:k. p(i) }.
Thm*  (least i:. p(i))  {i:k| p(i) & (j:i. p(j)) }		[least_characterized]
Thm*  m,k:, f:(mk). k<m  (x,y:m. x  y & f(x) = f(y))[pigeon_hole]
Thm*  Bij({u:| P(u) }; {v:| Q(v) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  (Bij({u:| P(u) & u = m }; {v:| Q(v) & v = k };
Thm*  (Bij(Replace value k by f(m) in f))		[delete_fenum_value_is_fenum_gen]
Thm*  Inj({u:| P(u) }; {v:| Q(v) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  (Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
Thm*  (Inj(Replace value k by f(m) in f))		[delete_fenum_value_is_inj_gen]
Thm*  Inj({u:| P(u) }; {v:| Q(v) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  ((Replace value k by f(m) in f)
Thm*  ( {u:| P(u) & u = m }{v:| Q(v) & v = k }
Thm*  (& Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
Thm*  (& Inj(Replace value k by f(m) in f))		[delete_fenum_value_is_inj_genW]
Thm*  Inj({u:| P(u) }; {u:| Q(u) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }.
Thm*  (f(i) = k
Thm*  (
Thm*  ((Replace value k by f(m) in f)(i) = f(i)  {v:| Q(v) & v = k })		[delete_fenum_value_comp2_gen]
Thm*  Inj({u:| P(u) }; {u:| Q(u) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }.
Thm*  (f(i) = k
Thm*  (
Thm*  ((Replace value k by f(m) in f)(i) = f(m)  {v:| Q(v) & v = k })		[delete_fenum_value_comp1_gen]
Thm*  Inj({k:| P(k) }; {k:| Q(k) }; f)
Thm*  
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  ((Replace value k by f(m) in f)
Thm*  ( {u:| P(u) & u = m }{v:| Q(v) & v = k })		[delete_fenum_value_wf_gen]
Def  Dedekind-Infinite(A) == a:A, f:(AA). Inj(A; A; f) & (x:A. f(x) = a)[Dedekind_infinite]
Def  (x:A. B(x)) ~ (x':A'. B'(x'))
Def  == f:(AA'), g:(A'A), F:(x:AB(x)B'(f(x))), G:(x:AB'(f(x))B(x)).
Def  == InvFuns(A;A';f;g) & (u:A. InvFuns(B(u);B'(f(u));F(u);G(u)))		[one_one_corr_fams]
Def  InvFuns(A;B;f;g) == (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y)[inv_funs_2]
Def  1-1 xA,yB. R(x;y)
Def  == x,x':A, y,y':B. R(x;y) & R(x';y')  (x = x'  y = y')		[rel_1_1_b]
Def  R is 1-1 == x,x':A, y,y':B. R(x,y) & R(x',y')  (x = x'  y = y')[rel_1_1]
Def  1-1-Corr x:A,y:B. R(x;y) == (x:A. !y:B. R(x;y)) & (y:B. !x:A. R(x;y))[is_one_one_corr_rel]

In prior sections: core int 1 bool 1 LogicSupplement int 2 num thy 1 SimpleMulFacts IteratedBinops rel 1

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

DiscreteMath Sections DiscrMathExt Doc