Thm* (AH ~ 8) ![](FONT/eq.png) ((AH {1...8}) ~ 64) | [chessboard_example] |
Thm* x:A. (x nil) ![](FONT/eq.png) False | [is_list_mem_null] |
Thm* f:( a![](FONT/dash.png) ![](FONT/then_med.png) 2).
Thm* ( i: a. P(i) ![](FONT/if_big.png) f(i) = 1 2) ![](FONT/eq.png) ({x: a| P(x) } ~ (Msize(f))) | [card_st_vs_msize] |
Thm* (![](FONT/exi.png) ( a onto b)) ![](FONT/eq.png) b a | [surj_typing_imp_le] |
Thm* (![](FONT/exi.png) ( a onto b)) ![](FONT/eq.png) (![](FONT/exi.png) ( b inj a)) | [nsub_surj_imp_a_rev_inj2] |
Thm* e:(B![](FONT/dash.png) B![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* IsEqFun(B;e)
Thm* ![](FONT/eq.png)
Thm* ( a: , f:( a onto B). ( y.least x: . (f(x)) e y) B inj a) | [nsub_surj_imp_a_rev_inj_gen] |
Thm* Dedekind-Infinite(A) ![](FONT/eq.png) Finite(A) | [dedekind_imp_nonfin] |
Thm* Dedekind-Infinite(A) ![](FONT/eq.png) Unbounded(A) | [dededing_imp_unb_inf] |
Thm* Dedekind-Infinite(A) ![](FONT/eq.png) Infinite(A) | [dedekind_inf_imp_inf] |
Thm* InvFuns(A;A;f;g) ![](FONT/eq.png) ( i: . InvFuns(A;A;f{ i};g{ i})) | [compose_iter_inverses] |
Thm* Bij(A; A; f) ![](FONT/eq.png) ( i: . Bij(A; A; f{ i})) | [compose_iter_bijection] |
Thm* Surj(A; A; f) ![](FONT/eq.png) ( i: . Surj(A; A; f{ i})) | [compose_iter_surjection] |
Thm* Inj(A; A; f) ![](FONT/eq.png) ( i: . Inj(A; A; f{ i})) | [compose_iter_injection] |
Thm* x:A, f:(A![](FONT/dash.png) A), i,j,k: . k = i j ![](FONT/eq.png) f{ i}{ j}(x) = f{ k}(x) A | [compose_iter_prod] |
Thm* f:(A![](FONT/dash.png) A), i,j,k: . k = i+j ![](FONT/eq.png) f{ i} o f{ j} = f{ k} | [compose_iter_sum_comp] |
Thm* x:A, f:(A![](FONT/dash.png) A), i,j,k: . k = i+j ![](FONT/eq.png) f{ i}(f{ j}(x)) = f{ k}(x) | [compose_iter_sum] |
Thm* f:(A![](FONT/dash.png) A), u:A. f(u) = u ![](FONT/eq.png) ( i: . f{ i}(u) = u) | [compose_iter_point_id] |
Thm* a,b: . (A ~ a) ![](FONT/eq.png) (B ~ b) ![](FONT/eq.png) ((A B) ~ (a b)) | [finite_indep_sum_card] |
Thm* a,b,c: . a b = c ![](FONT/eq.png) (( a![](FONT/x_big.png) b) ~ c) | [nsub_mul] |
Thm* c,a,b: . a+b = c ![](FONT/eq.png) (( a+ b) ~ c) | [nsub_add] |
Thm* a,b',b: . b = b'+1 ![](FONT/eq.png) ({a...b'} ~ {a..b }) | [intiseg_intseg] |
Thm* c,a: , b: . c = b-a ![](FONT/eq.png) ({a..b } ~ c) | [nsub_intseg] |
Thm* a,b,a',b': . b-a = b'-a' ![](FONT/eq.png) ({a..b } ~ {a'..b' }) | [intseg_shift] |
Thm* a,b: . b a ![](FONT/eq.png) (Void ~ {a..b }) | [intseg_void] |
Thm* (A ~ A') ![](FONT/eq.png) (B ~ B') ![](FONT/eq.png) ((A![](FONT/dash.png) B) ~ (A'![](FONT/dash.png) B')) | [function_functionality_wrt_one_one_corr] |
Thm* B,B':(A![](FONT/dash.png) Type). ( x:A. B(x) ~ B'(x)) ![](FONT/eq.png) ((x:A![](FONT/dash.png) B(x)) ~ (x:A![](FONT/dash.png) B'(x))) | [function_functionality_wrt_one_one_corr_B] |
Thm* (x:A. B(x)) ~ (x:A'. B'(x)) ![](FONT/eq.png) ((x:A![](FONT/dash.png) B(x)) ~ (x:A'![](FONT/dash.png) B'(x))) | [card_pi] |
Thm* a,b: , B:({a..b }![](FONT/dash.png) Type).
Thm* a<b ![](FONT/eq.png) ((i:{a..b } B(i)) ~ ((i:{a..(b-1) } B(i))+B(b-1))) | [card_split_end_sum_intseg_family] |
Thm* ( x:A. Dec( P(x))) ![](FONT/eq.png) (A ~ ({x:A| P(x) }+{x:A| P(x) })) | [card_split_decbl_squash] |
Thm* B:(A![](FONT/dash.png) Type), P:(A![](FONT/dash.png) Prop).
Thm* ( i:A. Dec(P(i)))
Thm* ![](FONT/eq.png)
Thm* ((i:A B(i)) ~ ((i:{i:A| P(i) } B(i))+(i:{i:A| P(i) } B(i)))) | [card_split_sigma_dom_decbl] |
Thm* ( x:A. Dec(P(x))) ![](FONT/eq.png) (A ~ ({x:A| P(x) }+{x:A| P(x) })) | [card_split_decbl] |
Thm* (A ~ A') ![](FONT/eq.png) (B ~ B') ![](FONT/eq.png) ((A B) ~ (A' B')) | [product_functionality_wrt_one_one_corr] |
Thm* B,B':(A![](FONT/dash.png) Type). ( x:A. B(x) ~ B'(x)) ![](FONT/eq.png) ((x:A B(x)) ~ (x:A B'(x))) | [product_functionality_wrt_one_one_corr_B] |
Thm* (x:A. B(x)) ~ (x:A'. B'(x)) ![](FONT/eq.png) ((x:A B(x)) ~ (x:A' B'(x))) | [card_sigma] |
Thm* ( x:A. B(x) ![](FONT/if_big.png) B'(x)) ![](FONT/eq.png) ({x:A| B(x) } ~ {x:A| B'(x) }) | [set_functionality_wrt_one_one_corr_n_pred] |
Thm* ( x:A. B(x) ![](FONT/if_big.png) B'(x)) ![](FONT/eq.png) ({x:A| B(x) } ~ {x:A| B'(x) }) | [set_functionality_wrt_one_one_corr_n_pred2] |
Thm* Bij(A; A'; f)
Thm* ![](FONT/eq.png)
Thm* ( x:A. B(x) ![](FONT/if_big.png) B'(f(x))) ![](FONT/eq.png) ({x:A| B(x) } ~ {x:A'| B'(x) }) | [card_settype_sq] |
Thm* Bij(A; A'; f)
Thm* ![](FONT/eq.png)
Thm* ( x:A. B(x) ![](FONT/if_big.png) B'(f(x))) ![](FONT/eq.png) ({x:A| B(x) } ~ {x:A'| B'(x) }) | [card_settype] |
Thm* (A ~ A') ![](FONT/eq.png) (B ~ B') ![](FONT/eq.png) ((A+B) ~ (A'+B')) | [union_functionality_wrt_one_one_corr] |
Thm* (A ~ A') ![](FONT/eq.png) (B ~ B') ![](FONT/eq.png) (:A. B) ~ (:A'. B') | [one_one_corr_fams_indep_if_one_one_corr] |
Thm* g:(A'![](FONT/dash.png) A). Bij(A'; A; g) ![](FONT/eq.png) (x:A. B(x)) ~ (x':A'. B(g(x'))) | [one_one_corr_fams_if_bij_A] |
Thm* ( x:A. B(x) ~ B'(x)) ![](FONT/eq.png) (x:A. B(x)) ~ (x:A. B'(x)) | [one_one_corr_fams_if_one_one_corr_B] |
Thm* f:(A![](FONT/dash.png) B). Bij(A; B; f) ![](FONT/eq.png) ( g:(B![](FONT/dash.png) A). InvFuns(A;B;f;g)) | [bij_imp_exists_inv2] |
Thm* P:(A![](FONT/dash.png) B![](FONT/dash.png) Prop). ( x:A. !y:B. P(x;y)) ![](FONT/eq.png) (A ~ (y:B {x:A| P(x;y) })) | [partition_type] |
Thm* (A ~ m) ![](FONT/eq.png) (A ~ k) ![](FONT/eq.png) m = k | [counting_is_unique] |
Thm* ( A:Type. Finite(A) ![](FONT/eq.png) Infinite(A)) ![](FONT/eq.png) ( D:Type. ![](FONT/not.png) (![](FONT/exi.png) D) ![](FONT/eq.png) (![](FONT/exi.png) D)) | [absurd_nonfinite_imp_infinite] |
Thm* ( A:Type. Finite(A) ![](FONT/if_big.png) Unbounded(A)) ![](FONT/if_big.png) ( P:Prop. ![](FONT/not.png) P ![](FONT/eq.png) P) | [nonfin_eqv_unb_inf_iff_negnegelim] |
Thm* ( A:Type. Finite(A) ![](FONT/eq.png) Unbounded(A)) ![](FONT/eq.png) ( D:Type. ![](FONT/not.png) (![](FONT/exi.png) D) ![](FONT/eq.png) (![](FONT/exi.png) D)) | [absurd_nonfin_imp_unb_inf] |
Thm* ( P:Prop. ![](FONT/not.png) P ![](FONT/eq.png) P) ![](FONT/eq.png) ( A:Type. Finite(A) ![](FONT/eq.png) Unbounded(A)) | [negnegelim_imp_notfin_imp_unb_inf] |
Thm* (A ~ B) ![](FONT/eq.png) Infinite(A) ![](FONT/eq.png) Infinite(B) | [ooc_preserves_infiniteness] |
Thm* (A ~ B) ![](FONT/eq.png) Unbounded(A) ![](FONT/eq.png) Unbounded(B) | [ooc_preserves_unb_inf] |
Thm* Infinite(A) ![](FONT/eq.png) Finite(A) | [infinite_imp_nonfinite] |
Thm* Unbounded(A) ![](FONT/eq.png) Finite(A) | [unb_inf_not_fin] |
Thm* f:(A![](FONT/dash.png) B). Bij(A; B; f) ![](FONT/eq.png) ( g:(B![](FONT/dash.png) A). InvFuns(A;B;f;g)) | [bij_imp_exists_inv_version2] |
Thm* f:(A![](FONT/dash.png) B), g:(B![](FONT/dash.png) A). InvFuns(A;B;f;g) ![](FONT/eq.png) Bij(A; B; f) | [fun_with_inv_is_bij_version2] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) Bij(B; A; g) | [fun_with_inv2_is_bij_rev] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) Bij(A; B; f) | [fun_with_inv2_is_bij] |
Thm* (A ![](FONT/eq.png) C) ![](FONT/eq.png) (B ![](FONT/eq.png) D) ![](FONT/eq.png) A & B ![](FONT/eq.png) C & D | [parallel_conjunct_imp] |
Thm* g:(B![](FONT/dash.png) A). Surj(A; B; f) ![](FONT/eq.png) ( x:A. g(f(x)) = x) ![](FONT/eq.png) ( y:B. f(g(y)) = y) | [left_inv_of_surj_is_right_inv] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) InvFuns(A;B;f;h) ![](FONT/eq.png) g = h | [inv_funs_2_unique] |
Thm* (A ~ B) ![](FONT/eq.png) (B ~ C) ![](FONT/eq.png) (A ~ C) | [one_one_corr_2_transitivity] |
Thm* (A ~ B) ![](FONT/eq.png) (B ~ A) | [one_one_corr_2_inversion] |
Thm* (A ~ A') ![](FONT/eq.png) (B ~ B') ![](FONT/eq.png) ((A ~ B) ![](FONT/if_big.png) (A' ~ B')) | [one_one_corr_2_functionality_wrt_one_one_corr] |
Thm* (A ~ B) ![](FONT/eq.png) ((![](FONT/exi.png) A) ![](FONT/if_big.png) (![](FONT/exi.png) B)) | [inhabited_functionality_wrt_one_one_corr] |
Thm* (A ~ B) ![](FONT/eq.png) (A ![](FONT/if_big.png) B) | [iff_weakening_wrt_one_one_corr_2] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) Surj(B; A; g) | [fun_with_inv2_is_surj_rev] |
Thm* (A ~ A') ![](FONT/eq.png) (B ~ B') ![](FONT/eq.png) ((A inj B) ~ (A' inj B')) | [injection_type_functionality_wrt_ooc] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) Inj(A; B; f) & Inj(B; A; g) | [invfuns_are_inj] |
Thm* (A ~ B) ![](FONT/eq.png) Dedekind-Infinite(A) ![](FONT/eq.png) Dedekind-Infinite(B) | [ooc_preserves_dededkind_inf] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) Inj(B; A; g) | [fun_with_inv2_is_inj_rev] |
Thm* B:(A![](FONT/dash.png) Type), B':(A'![](FONT/dash.png) Type).
Thm* (x:A. B(x)) ~ (x':A'. B'(x')) ![](FONT/eq.png) (x':A'. B'(x')) ~ (x:A. B(x)) | [one_one_corr_fams_sym] |
Thm* (A ~ A') ![](FONT/eq.png) (B ~ B') ![](FONT/eq.png) ((A onto B) ~ (A' onto B')) | [surjection_type_functionality_wrt_ooc] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) Surj(A; B; f) & Surj(B; A; g) | [invfuns_are_surj] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) InvFuns(B;A;g;f) | [inv_funs_2_sym] |
Thm* k: , B:( k![](FONT/dash.png) Type), Q:(x: k![](FONT/dash.png) B(x)![](FONT/dash.png) Prop).
Thm* ( x: k. y:B(x). Q(x;y)) ![](FONT/eq.png) ( f:(x: k![](FONT/dash.png) B(x)). x: k. Q(x;f(x))) | [dep_finite_choice] |
Thm* k: , Q:( k![](FONT/dash.png) A![](FONT/dash.png) Prop).
Thm* ( x: k. y:A. Q(x;y)) ![](FONT/eq.png) ( f:( k![](FONT/dash.png) A). x: k. Q(x;f(x))) | [finite_choice] |
Thm* ( x:A. Dec(P(x)))
Thm* ![](FONT/eq.png)
Thm* ((x:A![](FONT/dash.png) B(x)) ~ ((x:A st P(x)![](FONT/dash.png) B(x)) (x:A st P(x)![](FONT/dash.png) B(x)))) | [card_split_prod_intseg_family_decbl] |
Thm* Bij(A; B; g) ![](FONT/eq.png) Bij(B; C; f) ![](FONT/eq.png) Bij(A; C; f o g) | [comp_preserves_bij] |
Thm* A:Type, A',A'':Type, B:(A![](FONT/dash.png) Type), B':(A'![](FONT/dash.png) Type), B'':(A''![](FONT/dash.png) Type).
Thm* (x:A. B(x)) ~ (x':A'. B'(x'))
Thm* ![](FONT/eq.png)
Thm* (x':A'. B'(x')) ~ (x'':A''. B''(x'')) ![](FONT/eq.png) (x:A. B(x)) ~ (x'':A''. B''(x'')) | [one_one_corr_fams_trans] |
Thm* (A ~ A') ![](FONT/eq.png) (B ~ B') ![](FONT/eq.png) ((A![](FONT/if_med.png) B) ~ (A'![](FONT/if_med.png) B')) | [inv_pair_functionality_wrt_one_one_corr] |
Thm* f:(A onto B), a: . a onto A ![](FONT/eq.png) (B Discrete) ![](FONT/eq.png) Surj(A; B; f) | [surjection_type_surjection] |
Thm* Surj(A; B; g) ![](FONT/eq.png) Surj(B; C; f) ![](FONT/eq.png) Surj(A; C; f o g) | [comp_preserves_surj] |
Thm* Inj(A; B; g) ![](FONT/eq.png) Inj(B; C; f) ![](FONT/eq.png) Inj(A; C; f o g) | [comp_preserves_inj] |
Thm* Infinite(A) ![](FONT/eq.png) Unbounded(A) | [unboundedly_imp_productively_infinite] |
Thm* k,n: . k = n+1 ![](FONT/eq.png) k! = k n! ![](FONT/nat.png) | [factorial_via_intseg_step] |
Thm* P:{P:(![](FONT/nat.png) ![](FONT/dash.png) Prop)| i: . P(i) }.
Thm* ( i: . Dec(P(i))) ![](FONT/eq.png) (![](FONT/exi.png) {i: | P(i) & ( j: . j<i ![](FONT/eq.png) P(j)) }) | [least_exists2] |
Thm* k: , P:{P:( k![](FONT/dash.png) Prop)| i: k. P(i) }.
Thm* ( i: k. Dec(P(i))) ![](FONT/eq.png) (![](FONT/exi.png) {i: k| P(i) & ( j: i. P(j)) }) | [least_exists] |
Thm* a,a': . a'-a = 1 ![](FONT/eq.png) ( B:({a..a' }![](FONT/dash.png) Type). (i:{a..a' } B(i)) ~ B(a)) | [card_sum_family_intseg_singleton_elim] |
Thm* A = B ![](FONT/eq.png) (A ~ B) | [one_one_corr_2_weakening_wrt] |
Thm* a,a': . a'-a = 1 ![](FONT/eq.png) ( B:({a..a' }![](FONT/dash.png) Type). (i:{a..a' }![](FONT/dash.png) B(i)) ~ B(a)) | [card_prod_family_intseg_singleton_elim] |
Thm* k: , j: k, m: . m = k-1 ![](FONT/eq.png) ({i: k| i = j } ~ m) | [nsub_delete] |
Thm* a,a': .
Thm* a'-a = 1 ![](FONT/eq.png) ( B:({a..a' }![](FONT/dash.png) Type). (i:{a..a' } B(i)) ~ ({a: } B(a))) | [card_sum_family_singleton_vs_intseg] |
Thm* R:(A![](FONT/dash.png) A![](FONT/dash.png) Prop).
Thm* (![](FONT/exi.png) A) & (Trans x,y:A. R(x;y)) & ( x:A. y:A. R(x;y))
Thm* ![](FONT/eq.png)
Thm* ( k:![](FONT/nat.png) . f:( k![](FONT/dash.png) A). i,j: k. i<j ![](FONT/eq.png) R(f(i);f(j))) | [no_finite_model_lemma] |
Thm* (A ~ B) ![](FONT/eq.png) Finite(A) ![](FONT/eq.png) Finite(B) | [ooc_preserves_finiteness] |
Thm* e:(B![](FONT/dash.png) B![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* IsEqFun(B;e) ![](FONT/eq.png) ( a: , f:( a onto B), y:B. f(least x: . (f(x)) e y) = y) | [nsub_surj_least_preimage_works_gen] |
Thm* e:(B![](FONT/dash.png) B![](FONT/dash.png) ![](FONT/then_med.png) ).
Thm* IsEqFun(B;e) ![](FONT/eq.png) ( a: , f:( a onto B), y:B. (least x: . (f(x)) e y) a) | [nsub_surj_least_preimage_total_gen] |
Thm* (A Discrete) ![](FONT/eq.png) ( k: , f:( k inj A). f k bij {a:A| i: k. a = f(i) }) | [nsub_inj_discr_range_bijtype] |
Thm* (A Discrete)
Thm* ![](FONT/eq.png)
Thm* ( k: , f:( k inj A).
Thm* ({a:A| i: k. a = f(i) } Type
Thm* (& f k![](FONT/dash.png) {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) ![](FONT/eq.png) ( k: , f:( k![](FONT/dash.png) A). f k onto {a:A| i: k. a = f(i) }) | [nsub_discr_range_surjtype] |
Thm* (A Discrete)
Thm* ![](FONT/eq.png)
Thm* ( k: , f:( k![](FONT/dash.png) A).
Thm* ({a:A| i: k. a = f(i) } Type
Thm* (& f k![](FONT/dash.png) {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:(![](FONT/nat.png) ![](FONT/dash.png) ![](FONT/then_med.png) )| i: . p(i) }.
Thm* (least i: . p(i)) {i: | p(i) & ( j: . j<i ![](FONT/eq.png) p(j)) } | [least_characterized2] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) Surj(A; B; f) | [fun_with_inv2_is_surj] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) Inj(A; B; f) | [fun_with_inv2_is_inj] |
Thm* A = A' ![](FONT/eq.png) B = B' ![](FONT/eq.png) (A ~ B) = (A' ~ B') | [one_one_corr_2_functionality_wrt_eq] |
Thm* m,k: , f:( m![](FONT/dash.png) ![](FONT/then_med.png) k). k<m ![](FONT/eq.png) ( x,y: m. x y & f(x) = f(y)) | [pigeon_hole] |
Thm* m,k: , f:( m![](FONT/dash.png) ![](FONT/then_med.png) k). Inj( m; k; f) ![](FONT/eq.png) m k | [inj_imp_le2] |
Thm* (![](FONT/exi.png) ( m inj k)) ![](FONT/eq.png) m k | [inj_typing_imp_le] |
Thm* ( f:( m![](FONT/dash.png) ![](FONT/then_med.png) k). Inj( m; k; f)) ![](FONT/eq.png) m k | [inj_imp_le] |
Thm* m: , f:( m![](FONT/dash.png) ![](FONT/then_med.png) ). Inj( m; ; f) ![](FONT/eq.png) ( x: m, y: x. f(x) = f(y)) | [finite_inj_counter_example] |
Thm* Bij( (m+1); (k+1); f) ![](FONT/eq.png) Bij( m; k; Replace value k by f(m) in f) | [delete_fenum_value_is_fenum] |
Thm* Inj( (m+1); (k+1); f) ![](FONT/eq.png) Inj( m; k; Replace value k by f(m) in f) | [delete_fenum_value_is_inj] |
Thm* Inj( (m+1); (k+1); f)
Thm* ![](FONT/eq.png)
Thm* ( i: m. f(i) = k ![](FONT/eq.png) (Replace value k by f(m) in f)(i) = f(i) ![](FONT/memb.png) k) | [delete_fenum_value_comp2] |
Thm* Inj( (m+1); (k+1); f)
Thm* ![](FONT/eq.png)
Thm* ( i: m. f(i) = k ![](FONT/eq.png) (Replace value k by f(m) in f)(i) = f(m) ![](FONT/memb.png) k) | [delete_fenum_value_comp1] |
Thm* Inj( (m+1); (k+1); f) ![](FONT/eq.png) (Replace value k by f(m) in f) m![](FONT/dash.png) ![](FONT/then_med.png) k | [delete_fenum_value_wf] |
Thm* Bij({u: | P(u) }; {v: | Q(v) }; f)
Thm* ![](FONT/eq.png)
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* ![](FONT/eq.png)
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* ![](FONT/eq.png)
Thm* ( m:{u: | P(u) }, k:{v: | Q(v) }.
Thm* ((Replace value k by f(m) in f)
Thm* ( {u: | P(u) & u = m }![](FONT/dash.png) {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* ![](FONT/eq.png)
Thm* ( m:{u: | P(u) }, k:{v: | Q(v) }, i:{u: | P(u) & u = m }.
Thm* ( f(i) = k
Thm* (![](FONT/eq.png)
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* ![](FONT/eq.png)
Thm* ( m:{u: | P(u) }, k:{v: | Q(v) }, i:{u: | P(u) & u = m }.
Thm* (f(i) = k
Thm* (![](FONT/eq.png)
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* ![](FONT/eq.png)
Thm* ( m:{u: | P(u) }, k:{v: | Q(v) }.
Thm* ((Replace value k by f(m) in f)
Thm* ( {u: | P(u) & u = m }![](FONT/dash.png) {v: | Q(v) & v = k }) | [delete_fenum_value_wf_gen] |
Thm* (![](FONT/exi.png) A) ![](FONT/eq.png) ( ! (A inj B)) | [inj_from_empty_unique] |
Thm* a,a': .
Thm* a'-a = 1 ![](FONT/eq.png) ( B:({a..a' }![](FONT/dash.png) Type). (i:{a..a' } B(i)) =ext ({a: } B(a))) | [exteq_sum_family_singleton_vs_intseg] |
Thm* a,a': .
Thm* a'-a = 1 ![](FONT/eq.png) ( B:({a..a' }![](FONT/dash.png) Type). (i:{a..a' }![](FONT/dash.png) B(i)) =ext ({a: }![](FONT/dash.png) B(a))) | [exteq_prod_family_singleton_vs_intseg] |
Thm* a,a': . a'-a = 1 ![](FONT/eq.png) ({a..a' } =ext {a: }) | [exteq_singleton_vs_intseg] |
Thm* a,b: . a b ![](FONT/eq.png) (b -- a) = b-a | [ndiff_vs_diff] |
Def 1-1 x A,y B. R(x;y)
Def == x,x':A, y,y':B. R(x;y) & R(x';y') ![](FONT/eq.png) (x = x' ![](FONT/if_big.png) y = y') | [rel_1_1_b] |
Def R is 1-1 == x,x':A, y,y':B. R(x,y) & R(x',y') ![](FONT/eq.png) (x = x' ![](FONT/if_big.png) y = y') | [rel_1_1] |