x:A. B(x) == x:A
B(x)x:A. B(x) == x:AB(x)is mentioned by
 8)   ((AH {1...8}) ~ 64) | [chessboard_example] |
A:Type, xs:A List. xs  Type | [list_member_type_wf] |
| x:A. (x nil) False | [is_list_mem_null] |
x,a:A, ys:A List. (x a.ys)  x = a  (x ys) | [is_list_mem_split] |
| A:Type, a:A, xs:A List. (a xs) Prop | [is_list_mem_wf] |
 B, same_range_sep(A; B) | [same_range_sep_inj_eqv] |
| (A inj B)(A inj B)Prop | [same_range_sep_wf_inj] |
| B, same_range_sep(A; B) | [same_range_sep_eqv] |
| (AB)(AB)Prop | [same_range_sep_wf] |
p:(a {k}  ). {i:a| p(i) } ~ k | [card_st_sized_bool] |
| p:(a). {x:a| p(x) } ~ (size(a)(p)) | [card_st_vs_boolsize] |
| f:(a2).
Thm* ( i:a. P(i) f(i) = 1 2) ({x:a| P(x) } ~ (Msize(f))) | [card_st_vs_msize] |
| a {k} ) ~ (a {k} 2) | [card_boolset_vs_mset] |
| a,k:. a {k} Type | [sized_bool_wf] |
| a:. size(a) (a) | [boolsize_wf] |
| a,k,x:. a {k} {x...} Type | [sized_mset_wf5] |
a,k:. a {k}  Type | [sized_mset_wf4] |
a,k,x:, y: . a {k} {x...y} Type | [sized_mset_wf3] |
a,k,x:, y:. a {k} {x..y } Type | [sized_mset_wf2] |
| a,k:. a {k} Type | [sized_mset_wf] |
| k:. Msize (k) | [msize_wf] |
a bij a) ~ (a a) | [nsub_bij_ooc_invpair] |
| k inj k) ~ (k onto k) | [nsub_inj_ooc_nsub_surj] |
| k inj k) ~ (k bij k) | [nsub_inj_ooc_nsub_bij] |
| k inj k) =ext (k bij k) | [nsub_inj_exteq_nsub_bij] |
| k onto k) ~ (k bij k) | [nsub_surj_ooc_nsub_bij] |
| k onto k) =ext (k bij k) | [nsub_surj_exteq_nsub_bij] |
| k inj k) =ext (k onto k) | [nsub_inj_exteq_nsub_surj] |
 (a onto b)) b a | [surj_typing_imp_le] |
| (a onto b)) ((b inj a)) | [nsub_surj_imp_a_rev_inj2] |
f:(a bij a). InvFuns(a;a;f; y.least x:. f(x)= y) | [nsub_bij_least_preimage_inverse] |
| f:(a onto b). (y.least x:. f(x)=y) b inj a | [nsub_surj_imp_a_rev_inj] |
| e:(BB).
Thm* IsEqFun(B;e) Thm*
Thm* ( a:, f:(a onto B). (y.least x:. (f(x)) e y) B inj a) | [nsub_surj_imp_a_rev_inj_gen] |
 Finite(A) | [dedekind_imp_nonfin] |
| Unbounded(A) | [dededing_imp_unb_inf] |
| Infinite(A) | [dedekind_inf_imp_inf] |
(i:. InvFuns(A;A;f{ i};g{i})) | [compose_iter_inverses] |
| (i:. Bij(A; A; f{i})) | [compose_iter_bijection] |
| (i:. Surj(A; A; f{i})) | [compose_iter_surjection] |
| f:(A inj A), i:. f{i} A inj A | [compose_iter_injection2] |
| k:, f:(k inj k). i:. f{i} = Id kk | [iter_perm_cycles_uniform2] |
| k:, f:(k inj k). i:. u:k. f{i}(u) = u | [iter_perm_cycles_uniform] |
| k:, f:(k inj k), u:k. i:. f{i}(u) = u | [compose_iter_inj_cycles] |
| (i:. Inj(A; A; f{i})) | [compose_iter_injection] |
| f:(AA), i:. f{i} = f{i-1} o f | [compose_iter_pos_comp2] |
| f:(AA), i:, x:A. f{i}(x) = f{i-1}(f(x)) | [compose_iter_pos2] |
x:A, f:(AA), i,j:. f{i}{j}(x) = f{i j}(x) | [compose_iter_prod2] |
| x:A, f:(AA), i,j,k:. k = ij f{i}{j}(x) = f{k}(x) A | [compose_iter_prod] |
| f:(AA), k:, i:{0...k}. f{k} = f{i} o f{k-i} | [compose_iter_sum_comp_rw] |
| x:A, f:(AA), k:, i:{0...k}. f{k}(x) = f{i}(f{k-i}(x)) | [compose_iter_sum_rw] |
| f:(AA), i,j,k:. k = i+j f{i} o f{j} = f{k} | [compose_iter_sum_comp] |
| x:A, f:(AA), i,j,k:. k = i+j f{i}(f{j}(x)) = f{k}(x) | [compose_iter_sum] |
| i:. Id{i} = Id AA | [compose_iter_id] |
| f:(AA), i:. f{i} = f o f{i-1} | [compose_iter_pos_comp] |
| f:(AA), u:A. f(u) = u (i:. f{i}(u) = u) | [compose_iter_point_id] |
| f:(AA), i:, x:A. f{i}(x) = f(f{i-1}(x)) | [compose_iter_pos] |
| f:(AA). f{1} = f | [compose_iter_once] |
| f:(AA). f{0} = Id | [compose_iter_zero_id] |
| f:(AA), x:A. f{0}(x) = x | [compose_iter_zero] |
| k:. (k) ~ | [card_nat_vs_nat_tuple] |
| f:(AA), i:. f{i} AA | [compose_iter_wf] |
| xy:(). <0,0> = next_nat_pair(xy) | [next_nat_pair_not_zeroes] |
| (AB)) ~ (A ~ B) | [inv_pair_inv2] |
| B) ~ (A ~ B) | [inv_pair_inv] |
a:, b:(a). (i:ab(i)) ~ ( i:a. b(i)) | [card_sigma_vs_nsub_sigma] |
| a,b:. (a+b) ~ (a+b) | [nsub_add_rw] |
| BC) ~ (BAC) | [card_curry_simple2] |
a,b,c:. c (ab) = (ca)b | [exp_exp_reduce2] |
| a,b,c:. c(ab) = (cb)a | [exp_exp_reduce1] |
| a,b:. (ab) ~ (ba) | [card_fun_vs_nsub_exp] |
a:, b:(a). (i:ab(i)) ~ ( i:a. b(i)) | [card_pi_vs_nsub_pi] |
| k inj k) ~ (k!) | [nsub_inj_factorial] |
| a inj b) ~ (b!a) | [nsub_inj_factorial_tail] |
| b inj b) ~ (b!) | [nsub_inj_factorial2] |
| a,b:. (A ~ a) (B ~ b) ((AB) ~ (ab)) | [finite_indep_sum_card] |
| a,b,c:. a(bc) = (ab)c | [mul_assoc_from_cross_assoc] |
| a,b:. (ab) ~ (ab) | [nsub_mul_rw] |
| a,b,c:. ab = c ((ab) ~ c) | [nsub_mul] |
| c,a,b:. a+b = c ((a+b) ~ c) | [nsub_add] |
| a,b:, c:{a...b}. ({a..c}+{c..b}) ~ {a..b} | [intseg_split] |
| a,b:. {a...b} ~ (1+b-a) | [nsub_intiseg_rw] |
| a:, b:. {a...b} ~ {a..(b+1)} | [intiseg_intseg_plus] |
| a,b',b:. b = b'+1 ({a...b'} ~ {a..b}) | [intiseg_intseg] |
| a,b:. {a..b} ~ (b-a) | [nsub_intseg_rw] |
| c,a:, b:. c = b-a ({a..b} ~ c) | [nsub_intseg] |
| a:, b,c:. {a..b} ~ {(a+c)..(b+c)} | [intseg_shift_by] |
| a,b,a',b':. b-a = b'-a' ({a..b} ~ {a'..b'}) | [intseg_shift] |
| a,b:. ba (Void ~ {a..b}) | [intseg_void] |
| B(x))C(xy)) ~ (x:Ay:B(x)C(<x,y>)) | [card_sigma_distr] |
| B(x))C(z)) ~ (x:Ay:B(x)C(<x,y>)) | [card_curry] |
| BC) ~ (ABC) | [card_curry_simple] |
| (B ~ B') ((AB) ~ (A'B')) | [function_functionality_wrt_one_one_corr] |
| B,B':(AType). (x:A. B(x) ~ B'(x)) ((x:AB(x)) ~ (x:AB'(x))) | [function_functionality_wrt_one_one_corr_B] |
| ((x:AB(x)) ~ (x:A'B'(x))) | [card_pi] |
| a,b:, B:({a..b}Type).
Thm* a<b ((i:{a..b}B(i)) ~ ((i:{a..(b-1)}B(i))+B(b-1))) | [card_split_end_sum_intseg_family] |
| a,b:, c:{a...b}, B:({a..b}Type).
Thm* (i:{a..b }B(i)) ~ ((i:{a..c}B(i))+(i:{c..b}B(i))) | [card_split_sum_intseg_family] |
x:A. Dec( P(x))) (A ~ ({x:A| P(x) }+{x:A| P(x) })) | [card_split_decbl_squash] |
| 0) ~ A | [card_nsub0_union_2] |
| 0+A) ~ A | [card_nsub0_union] |
| B:(AType), P:(AProp).
Thm* ( i:A. Dec(P(i)))
Thm*
Thm* ((i:A B(i)) ~ ((i:{i:A| P(i) }B(i))+(i:{i:A| P(i) }B(i)))) | [card_split_sigma_dom_decbl] |
| B:(AType), P:(AProp).
Thm* (i:{i:A| P(i) } B(i)) ~ {v:(i:AB(i))| P(v/x,y. x) } | [card_sigma_st_dom] |
| x:A. Dec(P(x))) (A ~ ({x:A| P(x) }+{x:A| P(x) })) | [card_split_decbl] |
| 2if i=0 A else B fi) | [card_union_vs_sigma] |
| [card_union_swap] | |
| 2if i=0 A else B fi;union_to_sigma;sigma_to_union) | [union_sigma_inverses] |
| a,b:, c:{a...b}, B:({a..b}Type).
Thm* (i:{a..b }B(i)) ~ ((i:{a..c}B(i))(i:{c..b}B(i))) | [card_split_prod_intseg_family] |
| (B ~ B') ((AB) ~ (A'B')) | [product_functionality_wrt_one_one_corr] |
| {x:A| q = x A/E }) ~ A | [card_quotient] |
| B,B':(AType). (x:A. B(x) ~ B'(x)) ((x:AB(x)) ~ (x:AB'(x))) | [product_functionality_wrt_one_one_corr_B] |
| ((x:AB(x)) ~ (x:A'B'(x))) | [card_sigma] |
| x:A. B(x) B'(x)) ({x:A| B(x) } ~ {x:A| B'(x) }) | [set_functionality_wrt_one_one_corr_n_pred] |
| x:A. B(x) B'(x)) ({x:A| B(x) } ~ {x:A| B'(x) }) | [set_functionality_wrt_one_one_corr_n_pred2] |
Thm*
Thm* ( x:A. B(x) B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) }) | [card_settype_sq] |
Thm*
Thm* ( x:A. B(x) B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) }) | [card_settype] |
| B) ~ (BA) | [card_product_swap] |
| A:Type, n:, x:A, xs:((n-1)A). [x/ xs] nA | [seq_cons_wf] |
| (B ~ B') ((A+B) ~ (A'+B')) | [union_functionality_wrt_one_one_corr] |
| (B ~ B') (:A. B) ~ (:A'. B') | [one_one_corr_fams_indep_if_one_one_corr] |
| g:(A'A). Bij(A'; A; g) (x:A. B(x)) ~ (x':A'. B(g(x'))) | [one_one_corr_fams_if_bij_A] |
| x:A. B(x) ~ B'(x)) (x:A. B(x)) ~ (x:A. B'(x)) | [one_one_corr_fams_if_one_one_corr_B] |
| f is 1-1 corr | [bij_iff_is_1_1_corr] |
| f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A;B;f;g)) | [bij_imp_exists_inv2] |
| P:(ABProp). (x:A. !y:B. P(x;y)) (A ~ (y:B{x:A| P(x;y) })) | [partition_type] |
| a,b:. (a ~ b) a = b | [fin_card_vs_nat_eq] |
| m) (A ~ k) m = k | [counting_is_unique] |
| A:Type. Finite(A) Infinite(A)) (D:Type. (D) (D)) | [absurd_nonfinite_imp_infinite] |
| A:Type. Finite(A) Unbounded(A)) (P:Prop. P P) | [nonfin_eqv_unb_inf_iff_negnegelim] |
| A:Type. Finite(A) Unbounded(A)) (D:Type. (D) (D)) | [absurd_nonfin_imp_unb_inf] |
| k:. Infinite(k) | [nsub_not_infinite] |
| P:Prop. P P) (A:Type. Finite(A) Unbounded(A)) | [negnegelim_imp_notfin_imp_unb_inf] |
| f:(AB). Bij(A; B; f)) (B ~ A) | [bij_iff_1_1_corr_version2a] |
| Infinite(A) Infinite(B) | [ooc_preserves_infiniteness] |
| Unbounded(A) Unbounded(B) | [ooc_preserves_unb_inf] |
| Finite(A) | [infinite_imp_nonfinite] |
| Finite(A) | [unb_inf_not_fin] |
| f:(AB). Bij(A; B; f)) (A ~ B) | [bij_iff_1_1_corr_version2] |
| f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A;B;f;g)) | [bij_imp_exists_inv_version2] |
| f:(AB), g:(BA). InvFuns(A;B;f;g) Bij(A; B; f) | [fun_with_inv_is_bij_version2] |
| f:(AB). (x.f(x)) = f | [eta_conv_version2] |
| f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f AD | [comp_assoc_version2] |
| f:(AB). Id o f = f AB | [comp_id_l_version2] |
| f:(AB). f o Id = f AB | [comp_id_r_version2] |
| Bij(B; A; g) | [fun_with_inv2_is_bij_rev] |
| Bij(A; B; f) | [fun_with_inv2_is_bij] |
| C) (B D) A & B C & D | [parallel_conjunct_imp] |
| g:(BA). Surj(A; B; f) (x:A. g(f(x)) = x) (y:B. f(g(y)) = y) | [left_inv_of_surj_is_right_inv] |
| InvFuns(A;B;f;h) g = h | [inv_funs_2_unique] |
| (B ~ C) (A ~ C) | [one_one_corr_2_transitivity] |
| (B ~ A) | [one_one_corr_2_inversion] |
| [one_one_corr_2_reflex] | |
| (B ~ B') ((A ~ B) (A' ~ B')) | [one_one_corr_2_functionality_wrt_one_one_corr] |
| ((A) (B)) | [inhabited_functionality_wrt_one_one_corr] |
| (A B) | [iff_weakening_wrt_one_one_corr_2] |
| Surj(B; A; g) | [fun_with_inv2_is_surj_rev] |
| (B ~ B') ((A inj B) ~ (A' inj B')) | [injection_type_functionality_wrt_ooc] |
| Inj(A; B; f) & Inj(B; A; g) | [invfuns_are_inj] |
| Dedekind-Infinite(A) Dedekind-Infinite(B) | [ooc_preserves_dededkind_inf] |
| Inj(B; A; g) | [fun_with_inv2_is_inj_rev] |
| B:(AType), B':(A'Type).
Thm* (x:A. B(x)) ~ (x':A'. B'(x')) (x':A'. B'(x')) ~ (x:A. B(x)) | [one_one_corr_fams_sym] |
| (B ~ B') ((A onto B) ~ (A' onto B')) | [surjection_type_functionality_wrt_ooc] |
| Surj(A; B; f) & Surj(B; A; g) | [invfuns_are_surj] |
| InvFuns(B;A;g;f) | [inv_funs_2_sym] |
| 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] |
| k:, Q:(kAProp).
Thm* ( x:k. y:A. Q(x;y)) (f:(kA). x:k. Q(x;f(x))) | [finite_choice] |
| x:A. Dec(P(x)))
Thm*
Thm* ((x:A B(x)) ~ ((x:A st P(x)B(x))(x:A st P(x)B(x)))) | [card_split_prod_intseg_family_decbl] |
| 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] |
| Bij(B; C; f) Bij(A; C; f o g) | [comp_preserves_bij] |
| A:Type, B:Type. (A ~~ B) (A ~ B) | [one_one_corr_iff_one_one_corr_2] |
| InvFuns(A;B;f;g) | [inv_funs_iff_inv_funs_2] |
| A:Type, A',A'':Type, B:(AType), B':(A'Type), B'':(A''Type).
Thm* (x:A. B(x)) ~ (x':A'. B'(x')) Thm*
Thm* (x':A'. B'(x')) ~ (x'':A''. B''(x'')) (x:A. B(x)) ~ (x'':A''. B''(x'')) | [one_one_corr_fams_trans] |
| (B ~ B') ((AB) ~ (A'B')) | [inv_pair_functionality_wrt_one_one_corr] |
| f:(a onto b). Surj(a; b; f) | [surjection_type_nsub_surjection] |
| f:(A onto B), a:. a onto A (B Discrete) Surj(A; B; f) | [surjection_type_surjection] |
| f:(B onto C), g:(A onto B). f o g A onto C | [compose_wf_surj] |
| Surj(B; C; f) Surj(A; C; f o g) | [comp_preserves_surj] |
| A,B,C:Type, f:(B inj C), g:(A inj B). f o g A inj C | [compose_wf_inj] |
| Inj(B; C; f) Inj(A; C; f o g) | [comp_preserves_inj] |
| a,a':A, x:(a = a'). x = * | [eq_mem_is_ax] |
| b,a:. b(b -- a)+a | [ndiff_bound] |
| a,b:. (a -- b) | [ndiff_wf_nat] |
| A:Type. Dedekind-Infinite(A) Prop | [Dedekind_infinite_wf] |
| Unbounded(A) | [unboundedly_imp_productively_infinite] |
| A:Type. Infinite(A) Prop | [productively_infinite_wf] |
| A:Type. Unbounded(A) Prop | [unboundedly_infinite_wf] |
| k:. k! = k(k-1)! | [factorial_via_intseg_step_rw] |
| k,n:. k = n+1 k! = kn! | [factorial_via_intseg_step] |
| A:Type. fin_enum(A) Type | [fin_enum_wf] |
| (AB)) (A ~ B) | [inv_pair_iff_ooc] |
| A,B:Type. sigma_to_union (i:2if i=0 A else B fi)(A+B) | [sigma_to_union_wf] |
| A,B:Type. union_to_sigma (A+B)(i:2if i=0 A else B fi) | [union_to_sigma_wf] |
| P:{P:(Prop)| i:. P(i) }.
Thm* ( i:. Dec(P(i))) ({i:| P(i) & (j:. j<i P(j)) }) | [least_exists2] |
| k:, P:{P:(kProp)| i:k. P(i) }.
Thm* ( i:k. Dec(P(i))) ({i:k| P(i) & (j:i. P(j)) }) | [least_exists] |
| (!i:2. if i=0 P else P fi) | [decidable_vs_unique_nsub2] |
| [one_one_corr_fams_refl] | |
| A:Type, A':Type, B:(AType), B':(A'Type).
Thm* ((x:A. B(x)) ~ (x':A'. B'(x'))) Prop | [one_one_corr_fams_wf] |
| a,a':. a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a)) | [card_sum_family_intseg_singleton_elim] |
| B:({a:A}Type). (i:{a:A}B(i)) ~ B(a) | [card_sum_family_singleton_elim] |
| 0) (A) | [card0_iff_uninhabited] |
| (A ~ B) | [one_one_corr_2_weakening_wrt] |
| B(x) } ~ {x:A| B(x) } | [subset_sq_remove_card] |
| a,a':. a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a)) | [card_prod_family_intseg_singleton_elim] |
| B(i)) ~ B(a) | [card_prod_family_singleton_elim] |
| a,b:. (a inj b) ~ (b((a-1) inj (b-1))) | [card_nsub_inj_vs_lopped] |
| k:, j:k. {i:k| i = j } ~ (k-1) | [nsub_delete_rw] |
| k:, j:k, m:. m = k-1 ({i:k| i = j } ~ m) | [nsub_delete] |
| 0A) ~ 1 | [card_void_dom_fun_unit] |
| 1) (!A) | [card1_iff_inhabited_uniquely] |
| a,a':.
Thm* a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ ({a:}B(a))) | [card_sum_family_singleton_vs_intseg] |
| [card_subset_vs_and] | |
| P(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi | [ifthenelse_distr_subtype_ooc] |
B) ~ ((A inj B) (A onto B)) | [bijtype_ooc_inj_isect_surjtype] |
| BC) ~ ((AB)C) | [simple_card_cross_assoc] |
| (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] |
| 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] |
| Finite(A) Finite(B) | [ooc_preserves_finiteness] |
| k:. Finite(k) | [nsub_is_finite] |
| A:Type. Finite(A) Prop | [is_finite_type_wf] |
| k:. (k+) ~ | [fin_plus_nat_ooc_nat] |
| f:(a onto b), y:b. f(least x:. f(x)=y) = y | [nsub_surj_least_preimage_works] |
| e:(BB).
Thm* IsEqFun(B;e) (a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y) | [nsub_surj_least_preimage_works_gen] |
| f:(a onto b), y:b. (least x:. f(x)=y) a | [nsub_surj_least_preimage_total] |
| e:(BB).
Thm* IsEqFun(B;e) (a:, f:(a onto B), y:B. (least x:. (f(x)) e y) a) | [nsub_surj_least_preimage_total_gen] |
| (k:, f:(k inj A). f k bij {a:A| i:k. a = f(i) }) | [nsub_inj_discr_range_bijtype] |
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] |
| (k:, f:(kA). f k onto {a:A| i:k. a = f(i) }) | [nsub_discr_range_surjtype] |
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] |
| p:{p:()| i:. p(i) }. p(least i:. p(i)) | [least_satisfies2] |
| p:{p:()| i:. p(i) }, j:(least i:. p(i)). p(j) | [least_is_least2] |
| k:, p:{p:(k)| i:k. p(i) }, j:(least i:. p(i)). p(j) | [least_is_least] |
| k:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i)) | [least_satisfies] |
| p:{p:()| i:. p(i) }. (least i:. p(i)) | [least_wf2] |
| p:{p:()| i:. p(i) }.
Thm* (least i: . p(i)) {i:| p(i) & (j:. j<i p(j)) } | [least_characterized2] |
| k:, p:{p:(k)| i:k. p(i) }. (least i:. p(i)) k | [least_wf] |
| k:, p:{p:(k)| i:k. p(i) }.
Thm* (least i: . p(i)) {i:k| p(i) & (j:i. p(j)) } | [least_characterized] |
| f:(AB), g:(BA). SqStable(InvFuns(A;B;f;g)) | [sq_stable__inv_funs_2] |
| Surj(A; B; f) | [fun_with_inv2_is_surj] |
| Inj(A; B; f) | [fun_with_inv2_is_inj] |
| B = B' (A ~ B) = (A' ~ B') | [one_one_corr_2_functionality_wrt_eq] |
| A,B:Type. (A ~ B) Prop | [one_one_corr_2_wf] |
| [inv_funs_2_identity] | |
| R:(ABProp). (R is 1-1) = (1-1 xA,yB. R(x;y)) | [rel_1_1_eq_rel_1_1_b] |
| A,B:Type, R:(ABProp). (R is 1-1) Type | [rel_1_1_wf] |
| A,B:Type, R:(ABType). (1-1 xA,yB. R(x;y)) Type | [rel_1_1_b_wf] |
m,k:, f:(mk). k<m (x,y:m. x  y & f(x) = f(y)) | [pigeon_hole] |
| m,k:, f:(mk). Inj(m; k; f) mk | [inj_imp_le2] |
| (m inj k)) mk | [inj_typing_imp_le] |
| f:(mk). Inj(m; k; f)) mk | [inj_imp_le] |
| m:, f:(m). Inj(m; ; f) (x:m, y:x. f(x) = f(y)) | [finite_inj_counter_example] |
| (m+1); (k+1); f) Bij(m; k; Replace value k by f(m) in f) | [delete_fenum_value_is_fenum] |
| (m+1); (k+1); f) Inj(m; k; Replace value k by f(m) in f) | [delete_fenum_value_is_inj] |
| (m+1); (k+1); f)
Thm*
Thm* ( i:m. f(i) = k (Replace value k by f(m) in f)(i) = f(i) k) | [delete_fenum_value_comp2] |
| (m+1); (k+1); f)
Thm*
Thm* ( i:m. f(i) = k (Replace value k by f(m) in f)(i) = f(m) k) | [delete_fenum_value_comp1] |
| (m+1); (k+1); f) (Replace value k by f(m) in f) mk | [delete_fenum_value_wf] |
| | 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] |
| | 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] |
| | 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] |
| | 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] |
| | 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] |
| | 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] |
| A,X:Type, P:(A), y:A, f:(XA).
Thm* (Replace values x s.t. P(x) by y in f) XA | [replace_fn_values_wf] |
| B) =ext ((A inj B)(A onto B)) | [bijtype_exteq_inj_isect_surjtype] |
B)  (A onto B) | [bijection_type_inc_surj] |
| B) (A onto B) | [bijtype_sub_surjtype] |
| A,B:Type. A onto B Type | [surjection_type_wf] |
| a:, b:, j:b, f:((a-1) inj {x:b| x = j }).
Thm* ( i.if i=a-1 j else f(i) fi) a inj b | [nsub_inj_fill_typing] |
| a:, b:, f:(a inj b). f (a-1) inj {x:b| x = f(a-1) } | [nsub_inj_lop_typing] |
| B) (A inj B) | [bijection_type_inc_inj] |
| B) (A inj B) | [bijtype_sub_injtype] |
| (A) (!(A inj B)) | [inj_from_empty_unique] |
| f:(A inj B), a:A. f {x:A| x = a } inj {y:B| y = f(a) } | [inj_point_deletion_inj] |
| f:(A inj B), a:A. f {x:A| x = a }{y:B| y = f(a) } | [inj_point_deletion] |
| f:(A inj B). Inj(A; B; f) | [injection_type_injection] |
| f:(A inj B). f AB | [injection_type_fun] |
| (A inj B)) (f:(AB). Inj(A; B; f)) | [injtype_vs_inj] |
| A,B:Type. A inj B Type | [injection_type_wf] |
| A,B:Type. A bij B Type | [bijection_type_wf] |
| a,a':.
Thm* a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a))) | [exteq_sum_family_singleton_vs_intseg] |
| a,a':.
Thm* a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a))) | [exteq_prod_family_singleton_vs_intseg] |
| a,a':. a'-a = 1 ({a..a'} =ext {a:}) | [exteq_singleton_vs_intseg] |
| i,j:. Dec(i = j) | [decidable__nat_equal] |
| b;i,j. i=j) | [eq_int_is_eq_nsub] |
| a,b:. ab (b -- a) = b-a | [ndiff_vs_diff] |
| A,B:Type, R:(ABProp). (1-1-Corr x:A,y:B. R(x;y)) Prop | [is_one_one_corr_rel_wf] |
| f,g. j:B. (i:A. f(i) = j) (i:A. g(i) = j) | [same_range_sep] |
| k:. (k inj A) | [unboundedly_infinite] |
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] |
| x:A. g(f(x)) = x) & (y:B. f(g(y)) = y) | [inv_funs_2] |
| A,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] |
| x,x':A, y,y':B. R(x,y) & R(x',y') (x = x' y = y') | [rel_1_1] |
| x:A. !y:B. R(x;y)) & (y:B. !x:A. R(x;y)) | [is_one_one_corr_rel] |
In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2 union num thy 1 SimpleMulFacts IteratedBinops
Try larger context:
DiscrMathExt
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html