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* InvFuns(A;B;f;g) ![](FONT/eq.png) Inj(A; B; f) & Inj(B; A; g) | [invfuns_are_inj] |
Thm* InvFuns(A;B;f;g) ![](FONT/eq.png) Surj(A; B; f) & Surj(B; A; g) | [invfuns_are_surj] |
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* 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* {x:{x:A| P(x) }| Q(x) } ~ {x:A| P(x) & Q(x) } | [card_subset_vs_and] |
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* 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* k: , p:{p:( k![](FONT/dash.png) ![](FONT/then_med.png) )| i: k. p(i) }.
Thm* (least i: . p(i)) {i: k| p(i) & ( j: i. p(j)) } | [least_characterized] |
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* 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] |
Def Dedekind-Infinite(A) == a:A, f:(A![](FONT/dash.png) A). Inj(A; A; f) & ( x:A. f(x) = a) | [Dedekind_infinite] |
Def (x:A. B(x)) ~ (x':A'. B'(x'))
Def == f:(A![](FONT/dash.png) A'), g:(A'![](FONT/dash.png) A), F:(x:A![](FONT/dash.png) B(x)![](FONT/dash.png) B'(f(x))), G:(x:A![](FONT/dash.png) B'(f(x))![](FONT/dash.png) 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 InvFuns(A;B;f;g) == ( x:A. g(f(x)) = x) & ( y:B. f(g(y)) = y) | [inv_funs_2] |
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] |
Def 1-1-Corr x:A,y:B. R(x;y) == ( x:A. !y:B. R(x;y)) & ( y:B. !x:A. R(x;y)) | [is_one_one_corr_rel] |