Thm* p:( a {k} ). {i: a| p(i) } ~ k | [card_st_sized_bool] |
Thm* p:( a![](FONT/dash.png) ![](FONT/then_med.png) ). {x: a| p(x) } ~ ( size( a)(p)) | [card_st_vs_boolsize] |
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* ( a {k} ) ~ ( a {k} 2) | [card_boolset_vs_mset] |
Thm* a,k: . a {k} Type | [sized_bool_wf] |
Thm* a: . size( a) ( a![](FONT/dash.png) ![](FONT/then_med.png) )![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/nat.png) | [boolsize_wf] |
Thm* a,k,x: . a {k} {x...} Type | [sized_mset_wf5] |
Thm* a,k: . a {k} ![](FONT/nat.png) Type | [sized_mset_wf4] |
Thm* a,k,x: , y: . a {k} {x...y} Type | [sized_mset_wf3] |
Thm* a,k,x: , y: . a {k} {x..y } Type | [sized_mset_wf2] |
Thm* a,k: . a {k} Type | [sized_mset_wf] |
Thm* k: . Msize ( k![](FONT/dash.png) ![](FONT/then_med.png) )![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/nat.png) | [msize_wf] |
Thm* ( a bij a) ~ ( a![](FONT/if_med.png) ![](FONT/then_med.png) a) | [nsub_bij_ooc_invpair] |
Thm* ( k inj k) ~ ( k onto k) | [nsub_inj_ooc_nsub_surj] |
Thm* ( k inj k) ~ ( k bij k) | [nsub_inj_ooc_nsub_bij] |
Thm* ( k inj k) =ext ( k bij k) | [nsub_inj_exteq_nsub_bij] |
Thm* ( k onto k) ~ ( k bij k) | [nsub_surj_ooc_nsub_bij] |
Thm* ( k onto k) =ext ( k bij k) | [nsub_surj_exteq_nsub_bij] |
Thm* ( k inj k) =ext ( k onto k) | [nsub_inj_exteq_nsub_surj] |
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* f:( a bij a). InvFuns( a; a;f; y.least x: . f(x)= y) | [nsub_bij_least_preimage_inverse] |
Thm* f:( a onto b). ( y.least x: . f(x)= y) b inj a | [nsub_surj_imp_a_rev_inj] |
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* 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* f:(A inj A), i: . f{ i} A inj A | [compose_iter_injection2] |
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* 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: . f{ i}{ j}(x) = f{ i j}(x) | [compose_iter_prod2] |
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), k: , i:{0...k}. f{ k} = f{ i} o f{ k-i} | [compose_iter_sum_comp_rw] |
Thm* x:A, f:(A![](FONT/dash.png) A), k: , i:{0...k}. f{ k}(x) = f{ i}(f{ k-i}(x)) | [compose_iter_sum_rw] |
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* i: . Id{ i} = Id A![](FONT/dash.png) A | [compose_iter_id] |
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* (k:![](FONT/nat.png) ![](FONT/x_big.png) k![](FONT/dash.png) ![](FONT/then_med.png) ) ~ ![](FONT/nat.png) | [card_nat_vs_nat_tuples_all] |
Thm* (k:![](FONT/nat.png) ![](FONT/plus.png) ![](FONT/x_big.png) k![](FONT/dash.png) ![](FONT/then_med.png) ) ~ ![](FONT/nat.png) | [card_nat_vs_nat_tuples] |
Thm* k:![](FONT/nat.png) . ( k![](FONT/dash.png) ![](FONT/then_med.png) ) ~ ![](FONT/nat.png) | [card_nat_vs_nat_tuple] |
Thm* (![](FONT/nat.png) ![](FONT/x_big.png) ) ~ ![](FONT/nat.png) | [card_nat_vs_nat_nat] |
Thm* f:(A![](FONT/dash.png) A), i: . f{ i} A![](FONT/dash.png) A | [compose_iter_wf] |
Thm* Bij( ; ![](FONT/nat.png) ![](FONT/x_big.png) ; nat_to_nat_pair) | [nat_to_nat_pair_bij] |
Thm* Surj( ; ![](FONT/nat.png) ![](FONT/x_big.png) ; nat_to_nat_pair) | [nat_to_nat_pair_surj] |
Thm* Inj( ; ![](FONT/nat.png) ![](FONT/x_big.png) ; nat_to_nat_pair) | [nat_to_nat_pair_inj] |
Thm* nat_to_nat_pair ![](FONT/nat.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/nat.png) ![](FONT/x_big.png) ![](FONT/nat.png) | [nat_to_nat_pair_wf] |
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* Inj(![](FONT/nat.png) ![](FONT/x_big.png) ; ![](FONT/nat.png) ![](FONT/x_big.png) ; next_nat_pair) | [next_nat_pair_inj] |
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* next_nat_pair ![](FONT/nat.png) ![](FONT/x_big.png) ![](FONT/nat.png) ![](FONT/dash.png) ![](FONT/then_med.png) ![](FONT/nat.png) ![](FONT/x_big.png) ![](FONT/nat.png) | [next_nat_pair_wf] |
Thm* a: , b:( a![](FONT/dash.png) ![](FONT/then_med.png) ). (i: a![](FONT/x_big.png) b(i)) ~ ( i: a. b(i)) | [card_sigma_vs_nsub_sigma] |
Thm* a,b: . ( a+ b) ~ (a+b) | [nsub_add_rw] |
Thm* a,b,c: . c (a b) = (c a) b | [exp_exp_reduce2] |
Thm* a,b,c: . c (a b) = (c b) a | [exp_exp_reduce1] |
Thm* a,b: . ( a![](FONT/dash.png) ![](FONT/then_med.png) b) ~ (b a) | [card_fun_vs_nsub_exp] |
Thm* a: , b:( a![](FONT/dash.png) ![](FONT/then_med.png) ). (i: a![](FONT/dash.png) ![](FONT/then_med.png) b(i)) ~ ( i: a. b(i)) | [card_pi_vs_nsub_pi] |
Thm* ( k inj k) ~ (k!) | [nsub_inj_factorial] |
Thm* ( a inj b) ~ (b!a) | [nsub_inj_factorial_tail] |
Thm* ( b inj b) ~ (b!) | [nsub_inj_factorial2] |
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) = (a b) c | [mul_assoc_from_cross_assoc] |
Thm* a,b: . ( a![](FONT/x_big.png) b) ~ (a b) | [nsub_mul_rw] |
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* Finite( ) | [nat_not_finite] |
Thm* a,b: . ( a ~ b) ![](FONT/if_big.png) a = b | [fin_card_vs_nat_eq] |
Thm* (A ~ m) ![](FONT/eq.png) (A ~ k) ![](FONT/eq.png) m = k | [counting_is_unique] |
Thm* ((![](FONT/nat.png) ![](FONT/dash.png) ![](FONT/then_med.png) ) ~ ) | [not_nat_occ_natfuns] |
Thm* k: . Infinite( k) | [nsub_not_infinite] |
Thm* ~ ![](FONT/nat.png) | [int_ooc_nat] |
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* f:( a onto b). Surj( a; b; f) | [surjection_type_nsub_surjection] |
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* a,b: . (a -- b) ![](FONT/nat.png) | [ndiff_wf_nat] |
Thm* k:![](FONT/nat.png) . k! = k (k-1)! ![](FONT/nat.png) | [factorial_via_intseg_step_rw] |
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* 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* k: . Finite( k) | [nsub_is_finite] |
Thm* ![](FONT/nat.png) ~ ![](FONT/nat.png) | [nat_plus_ooc_nat] |
Thm* k: . ( k+ ) ~ ![](FONT/nat.png) | [fin_plus_nat_ooc_nat] |
Thm* f:( a onto b), y: b. f(least x: . f(x)= y) = y | [nsub_surj_least_preimage_works] |
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* f:( a onto b), y: b. (least x: . f(x)= y) a | [nsub_surj_least_preimage_total] |
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) }. 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* 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* 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* i,j: . Dec(i = j) | [decidable__nat_equal] |
Thm* IsEqFun( b;![](FONT/lam.png) i,j. i= j) | [eq_int_is_eq_nsub] |
Def a {k} == {p:( a![](FONT/dash.png) ![](FONT/then_med.png) )| size( a)(p) = k } | [sized_bool] |
Def a {k} T == {p:( a![](FONT/dash.png) T)| Msize(p) = k } | [sized_mset] |
Def Infinite(A) == ![](FONT/exi.png) ( inj A) | [productively_infinite] |
Def Unbounded(A) == k: . ![](FONT/exi.png) ( k inj A) | [unboundedly_infinite] |
Def fin_enum(A) == k:![](FONT/nat.png) ![](FONT/x_big.png) k![](FONT/if_med.png) A | [fin_enum] |
Def Finite(A) == n: . A ~ n | [is_finite_type] |