Thm* k: , f:( k inj k). i:![](FONT/nat.png) . f{ i} = Id k![](FONT/dash.png) ![](FONT/then_med.png) k | [iter_perm_cycles_uniform2] |
Thm* k: , f:( k inj k). i:![](FONT/nat.png) . u: k. f{ i}(u) = u | [iter_perm_cycles_uniform] |
Thm* k: , f:( k inj k), u: k. i:![](FONT/nat.png) . f{ i}(u) = u | [compose_iter_inj_cycles] |
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* ( f:(A![](FONT/dash.png) B). Bij(A; B; f)) ![](FONT/if_big.png) (B ~ A) | [bij_iff_1_1_corr_version2a] |
Thm* ( f:(A![](FONT/dash.png) B). Bij(A; B; f)) ![](FONT/if_big.png) (A ~ B) | [bij_iff_1_1_corr_version2] |
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* 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* 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* ( 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 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) }. p(least i: . p(i)) | [least_satisfies2] |
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* k: , p:{p:( k![](FONT/dash.png) ![](FONT/then_med.png) )| i: k. p(i) }. p(least i: . p(i)) | [least_satisfies] |
Thm* p:{p:(![](FONT/nat.png) ![](FONT/dash.png) ![](FONT/then_med.png) )| i: . p(i) }. (least i: . p(i)) ![](FONT/nat.png) | [least_wf2] |
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) }. (least i: . p(i)) k | [least_wf] |
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* ( 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* (![](FONT/exi.png) (A inj B)) ![](FONT/if_big.png) ( f:(A![](FONT/dash.png) B). Inj(A; B; f)) | [injtype_vs_inj] |
Def same_range_sep(A; B) == ![](FONT/lam.png) f,g. j:B. ( i:A. f(i) = j) ![](FONT/if_big.png) ( i:A. g(i) = j) | [same_range_sep] |
Def Dedekind-Infinite(A) == a:A, f:(A![](FONT/dash.png) A). Inj(A; A; f) & ( x:A. f(x) = a) | [Dedekind_infinite] |
Def f is 1-1 corr == g:(B![](FONT/dash.png) A). InvFuns(A;B;f;g) | [is_one_one_corr] |
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 Finite(A) == n: . A ~ n | [is_finite_type] |
Def A ~ B == f:(A![](FONT/dash.png) B), g:(B![](FONT/dash.png) A). InvFuns(A;B;f;g) | [one_one_corr_2] |