Def  P  Q == (P  Q) & (P  Q)

is mentioned by

Thm*  x,a:A, ys:A List. (x  a.ys)  x = a  (x  ys)	[is_list_mem_split]
Thm*  f:(a2).  Thm*  (i:a. P(i)  f(i) = 1  2)  ({x:a| P(x) } ~ (Msize(f)))	[card_st_vs_msize]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } ~ {x:A| B'(x) })	[set_functionality_wrt_one_one_corr_n_pred]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } ~ {x:A| B'(x) })	[set_functionality_wrt_one_one_corr_n_pred2]
Thm*  Bij(A; A'; f) Thm*   Thm*  (x:A. B(x)  B'(f(x)))  ({x:A| B(x) } ~ {x:A'| B'(x) })	[card_settype_sq]
Thm*  Bij(A; A'; f) Thm*   Thm*  (x:A. B(x)  B'(f(x)))  ({x:A| B(x) } ~ {x:A'| B'(x) })	[card_settype]
Thm*  Bij(A; B; f)  f is 1-1 corr	[bij_iff_is_1_1_corr]
Thm*  a,b:. (a ~ b)  a = b	[fin_card_vs_nat_eq]
Thm*  (A:Type. Finite(A)  Unbounded(A))  (P:Prop. P  P)	[nonfin_eqv_unb_inf_iff_negnegelim]
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*  (A ~ A')  (B ~ B')  ((A ~ B)  (A' ~ B'))	[one_one_corr_2_functionality_wrt_one_one_corr]
Thm*  (A ~ B)  ((A)  (B))	[inhabited_functionality_wrt_one_one_corr]
Thm*  (A ~ B)  (A  B)	[iff_weakening_wrt_one_one_corr_2]
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*  A:Type, B:Type. (A ~~ B)  (A ~ B)	[one_one_corr_iff_one_one_corr_2]
Thm*  InvFuns(A; B; f; g)  InvFuns(A;B;f;g)	[inv_funs_iff_inv_funs_2]
Thm*  ((AB))  (A ~ B)	[inv_pair_iff_ooc]
Thm*  Dec(P)  (!i:2. if i=0 P else P fi)	[decidable_vs_unique_nsub2]
Thm*  (A ~ 0)  (A)	[card0_iff_uninhabited]
Thm*  (A ~ 1)  (!A)	[card1_iff_inhabited_uniquely]
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  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]

In prior sections: core well fnd int 1 bool 1 rel 1 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