Thm* A:Type, a:A, xs:A List. (a xs) Prop | [is_list_mem_wf] |
Thm* same_range_sep(A; B) (A inj B)![](FONT/dash.png) (A inj B)![](FONT/dash.png) Prop | [same_range_sep_wf_inj] |
Thm* same_range_sep(A; B) (A![](FONT/dash.png) B)![](FONT/dash.png) (A![](FONT/dash.png) B)![](FONT/dash.png) Prop | [same_range_sep_wf] |
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* ( 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* B:(A![](FONT/dash.png) Type), P:(A![](FONT/dash.png) Prop).
Thm* (i:{i:A| P(i) } B(i)) ~ {v:(i:A B(i))| P(v/x,y. x) } | [card_sigma_st_dom] |
Thm* ( x:A. Dec(P(x))) ![](FONT/eq.png) (A ~ ({x:A| P(x) }+{x:A| P(x) })) | [card_split_decbl] |
Thm* (q:A/E {x:A| q = x A/E }) ~ A | [card_quotient] |
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* 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: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* ( 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 ![](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* 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* R:(A![](FONT/dash.png) B![](FONT/dash.png) Prop).
Thm* (1-1-Corr x:A,y:B. R(x;y))
Thm* ![](FONT/if_big.png)
Thm* ( f:(A![](FONT/dash.png) B), g:(B![](FONT/dash.png) A).
Thm* (InvFuns(A;B;f;g) & ( x:A, y:B. R(x;y) ![](FONT/if_big.png) y = f(x) & x = g(y))) | [one_one_corr_rel_vs_invfuns] |
Thm* A:Type. Dedekind-Infinite(A) Prop | [Dedekind_infinite_wf] |
Thm* A:Type. Infinite(A) Prop | [productively_infinite_wf] |
Thm* A:Type. Unbounded(A) Prop | [unboundedly_infinite_wf] |
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* Dec(P) ![](FONT/if_big.png) ( !i: 2. if i= 0 P else P fi) | [decidable_vs_unique_nsub2] |
Thm* A:Type, A':Type, B:(A![](FONT/dash.png) Type), B':(A'![](FONT/dash.png) Type).
Thm* ((x:A. B(x)) ~ (x':A'. B'(x'))) Prop | [one_one_corr_fams_wf] |
Thm* {x:A| B(x) } ~ {x:A| B(x) } | [subset_sq_remove_card] |
Thm* {x:{x:A| P(x) }| Q(x) } ~ {x:A| P(x) & Q(x) } | [card_subset_vs_and] |
Thm* {x:A| if b P(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi | [ifthenelse_distr_subtype_ooc] |
Thm* ( A:Type, 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* (& ( x:A. R(x;x))
Thm* (& Finite(A)) | [no_finite_model] |
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:Type. Finite(A) Prop | [is_finite_type_wf] |
Thm* A = A' ![](FONT/eq.png) B = B' ![](FONT/eq.png) (A ~ B) = (A' ~ B') | [one_one_corr_2_functionality_wrt_eq] |
Thm* A,B:Type. (A ~ B) Prop | [one_one_corr_2_wf] |
Thm* R:(A![](FONT/dash.png) B![](FONT/dash.png) Prop). (R is 1-1) = (1-1 x A,y B. R(x;y)) | [rel_1_1_eq_rel_1_1_b] |
Thm* A,B:Type, R:(A![](FONT/dash.png) B![](FONT/dash.png) Prop). (R is 1-1) Type | [rel_1_1_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* A,B:Type, R:(A![](FONT/dash.png) B![](FONT/dash.png) Prop). (1-1-Corr x:A,y:B. R(x;y)) Prop | [is_one_one_corr_rel_wf] |