DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  x:A. B(x) == x:AB(x)

is mentioned by

Thm*  k:, f:(k inj k). i:. f{i} = Id  kk[iter_perm_cycles_uniform2]
Thm*  k:, f:(k inj k). i:. u:k. f{i}(u) = u[iter_perm_cycles_uniform]
Thm*  k:, f:(k inj k), u:k. i:. f{i}(u) = u[compose_iter_inj_cycles]
Thm*  f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A;B;f;g))[bij_imp_exists_inv2]
Thm*  (f:(AB). Bij(A; B; f))  (B ~ A)[bij_iff_1_1_corr_version2a]
Thm*  (f:(AB). Bij(A; B; f))  (A ~ B)[bij_iff_1_1_corr_version2]
Thm*  f:(AB). Bij(A; B; f)  (g:(BA). InvFuns(A;B;f;g))[bij_imp_exists_inv_version2]
Thm*  k:, B:(kType), Q:(x:kB(x)Prop).
Thm*  (x:k. y:B(x). Q(x;y))  (f:(x:kB(x)). x:k. Q(x;f(x)))		[dep_finite_choice]
Thm*  k:, Q:(kAProp).
Thm*  (x:k. y:A. Q(x;y))  (f:(kA). x:k. Q(x;f(x)))		[finite_choice]
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*  (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*  (A Discrete)  (k:, f:(k inj A). f  k bij {a:A| i:k. a = f(i) })[nsub_inj_discr_range_bijtype]
Thm*  (A Discrete)
Thm*  
Thm*  (k:, f:(k inj A).
Thm*  ({a:A| i:k. a = f(i) }  Type
Thm*  (& f  k{a:A| i:k. a = f(i) }
Thm*  (& Bij(k; {a:A| i:k. a = f(i) }; f))		[nsub_inj_discr_range_bij]
Thm*  (A Discrete)  (k:, f:(kA). f  k onto {a:A| i:k. a = f(i) })[nsub_discr_range_surjtype]
Thm*  (A Discrete)
Thm*  
Thm*  (k:, f:(kA).
Thm*  ({a:A| i:k. a = f(i) }  Type
Thm*  (& f  k{a:A| i:k. a = f(i) }
Thm*  (& Surj(k; {a:A| i:k. a = f(i) }; f))		[nsub_discr_range_surj]
Thm*  p:{p:()| i:. p(i) }. p(least i:. p(i))[least_satisfies2]
Thm*  p:{p:()| i:. p(i) }, j:(least i:. p(i)). p(j)[least_is_least2]
Thm*  k:, p:{p:(k)| i:k. p(i) }, j:(least i:. p(i)). p(j)[least_is_least]
Thm*  k:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i))[least_satisfies]
Thm*  p:{p:()| i:. p(i) }. (least i:. p(i))  [least_wf2]
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) }. (least i:. p(i))  k[least_wf]
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*  (f:(mk). Inj(m; k; f))  mk[inj_imp_le]
Thm*  m:, f:(m). Inj(m; ; f)  (x:m, y:x. f(x) = f(y))[finite_inj_counter_example]
Thm*  ((A inj B))  (f:(AB). Inj(A; B; f))[injtype_vs_inj]
Def  same_range_sep(A; B) == f,g. j:B. (i:A. f(i) = j)  (i:A. g(i) = j)[same_range_sep]
Def  Dedekind-Infinite(A) == a:A, f:(AA). Inj(A; A; f) & (x:A. f(x) = a)[Dedekind_infinite]
Def  f is 1-1 corr == g:(BA). InvFuns(A;B;f;g)[is_one_one_corr]
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  Finite(A) == n:. A ~ n[is_finite_type]
Def  A ~ B == f:(AB), g:(BA). InvFuns(A;B;f;g)[one_one_corr_2]

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

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

DiscreteMath Sections DiscrMathExt Doc