Thm* Dedekind-Infinite(A) ![](FONT/eq.png) Finite(A) | [dedekind_imp_nonfin] |
Thm* InvFuns(![](FONT/nat.png) ![](FONT/x_big.png) ;{xy:(![](FONT/nat.png) ![](FONT/x_big.png) )| xy = <0,0> ![](FONT/nat.png) ![](FONT/x_big.png) };next_nat_pair;prev_nat_pair) | [next_nat_pair_vs_prev_nat_pair] |
Thm* prev_nat_pair {xy:(![](FONT/nat.png) ![](FONT/x_big.png) )| xy = <0,0> ![](FONT/nat.png) ![](FONT/x_big.png) }![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/nat.png) ![](FONT/x_big.png) ![](FONT/nat.png) | [prev_nat_pair_wf] |
Thm* xy:(![](FONT/nat.png) ![](FONT/x_big.png) ). <0,0> = next_nat_pair(xy) ![](FONT/nat.png) ![](FONT/x_big.png) ![](FONT/nat.png) | [next_nat_pair_not_zeroes] |
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* Finite( ) | [nat_not_finite] |
Thm* ((![](FONT/nat.png) ![](FONT/dash.png) ![](FONT/then_med.png) ) ~ ) | [not_nat_occ_natfuns] |
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* k: . Infinite( k) | [nsub_not_infinite] |
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* Infinite(A) ![](FONT/eq.png) Finite(A) | [infinite_imp_nonfinite] |
Thm* Unbounded(A) ![](FONT/eq.png) Finite(A) | [unb_inf_not_fin] |
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* 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 ~ 0) ![](FONT/if_big.png) (![](FONT/exi.png) A) | [card0_iff_uninhabited] |
Thm* k: , j: k. {i: k| i = j } ~ (k-1) | [nsub_delete_rw] |
Thm* k: , j: k, m: . m = k-1 ![](FONT/eq.png) ({i: k| i = j } ~ m) | [nsub_delete] |
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* p:{p:(![](FONT/nat.png) ![](FONT/dash.png) ![](FONT/then_med.png) )| i: . p(i) }, j: (least i: . p(i)). p(j) | [least_is_least2] |
Thm* k: , p:{p:( k![](FONT/dash.png) ![](FONT/then_med.png) )| i: k. p(i) }, j: (least i: . p(i)). p(j) | [least_is_least] |
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: , 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* 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* 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:![](FONT/nat.png) , 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] |
Thm* a:![](FONT/nat.png) , b: , f:( a inj b). f (a-1) inj {x: b| x = f(a-1) } | [nsub_inj_lop_typing] |
Thm* (![](FONT/exi.png) A) ![](FONT/eq.png) ( ! (A inj B)) | [inj_from_empty_unique] |
Thm* f:(A inj B), a:A. f {x:A| x = a } inj {y:B| y = f(a) } | [inj_point_deletion_inj] |
Thm* f:(A inj B), a:A. f {x:A| x = a }![](FONT/dash.png) {y:B| y = f(a) } | [inj_point_deletion] |
Def Dedekind-Infinite(A) == a:A, f:(A![](FONT/dash.png) A). Inj(A; A; f) & ( x:A. f(x) = a) | [Dedekind_infinite] |