Introduction | Introductory Remarks | |
def | is_one_one_corr_rel
|
One-one correlation as a relation
![]() ![]() ![]() ![]() |
def | is_list_mem
|
(![]() ![]() ![]() ![]() ![]() ![]() |
THM | ndiff_vs_diff
|
![]() ![]() ![]() ![]() ![]() |
THM | eq_int_is_eq_nsub
|
![]() ![]() ![]() ![]() |
THM | decidable__nat_equal
|
![]() ![]() |
THM | exteq_singleton_vs_intseg
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | exteq_prod_family_singleton_vs_intseg
|
![]() ![]() a'-a = 1 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | exteq_sum_family_singleton_vs_intseg
|
![]() ![]() a'-a = 1 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | injection_type
|
(the injections from ![]() ![]() ![]() |
def | bijection_type
|
(the bijections from ![]() ![]() ![]() |
THM | injtype_vs_inj
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | injection_type_fun
|
![]() ![]() ![]() ![]() ![]() |
THM | injection_type_injection
|
![]() ![]() |
THM | inj_point_deletion
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | inj_point_deletion_inj
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | inj_from_empty_unique
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | bijtype_sub_injtype
|
![]() ![]() ![]() |
THM | bijection_type_inc_inj
|
![]() ![]() ![]() |
THM | nsub_inj_lop_typing
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_inj_fill_typing
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | surjection_type
|
(the surjections from ![]() ![]() ![]() |
THM | bijtype_sub_surjtype
|
![]() ![]() ![]() |
THM | bijection_type_inc_surj
|
![]() ![]() ![]() |
THM | bijtype_exteq_inj_isect_surjtype
|
![]() ![]() ![]() ![]() |
COM | unicomp_assoc
|
![]() |
COM | inverse_function_intro
|
Explain inverse functions and
|
COM | one_one_corr_intro
| One-to-One Correspondence ... |
COM | one_one_corr_via_inverse
| One-to-One Correspondence via Inverse Functions ... |
COM | one_one_corr_intro_aux1
| Comparison of definitional resources used. ... |
COM | one_one_corr_intro3
| One-to-One Correspondence: equivalence of two characterizations. ... |
COM | count_demo
| Counting is finding a function of a certain kind. ... |
def | list_to_function
|
A function mapping positions in a list to entries
|
COM | note_on_generalization_for_induction
| Not done yet. |
def | replace_fn_values
|
![]() |
def | delete_fenum_value
|
Special purpose operation for shrinking the domain and range of an injection simultaneously. See ![]() |
COM | delete_fenum_value_example
|
![]() ![]() ![]() ![]() * ![]() [1; 3; 0; 7; 2; 5; 6] |
THM | delete_fenum_value_comp1_gen
|
![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() (f(i) = k ![]() ![]() ![]() ![]() ![]() |
THM | delete_fenum_value_comp2_gen
|
![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() |
THM | delete_fenum_value_is_inj_genW
|
![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ((Replace value k by f(m) in f) ![]() ![]() ![]() ![]() ![]() ![]() ![]() (& Inj({u: ![]() ![]() ![]() ![]() (& Inj(Replace value k by f(m) in f)) |
THM | delete_fenum_value_is_inj_gen
|
![]() ![]() ![]() ![]() ( ![]() ![]() ![]() (Inj({u: ![]() ![]() ![]() ![]() (Inj(Replace value k by f(m) in f)) |
THM | delete_fenum_value_is_fenum_gen
|
![]() ![]() ![]() ![]() ( ![]() ![]() ![]() (Bij({u: ![]() ![]() ![]() ![]() (Bij(Replace value k by f(m) in f)) |
THM | delete_fenum_value_comp1
|
![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() |
THM | delete_fenum_value_comp2
|
![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | delete_fenum_value_is_inj
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | delete_fenum_value_is_fenum
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | finite_inj_counter_example
(Proof Gloss) |
Lemma for the A finite non-injection into integers maps some two distinct arguments to the same value. ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | inj_imp_le
(Proof Gloss) |
The range of a finite injection is as big as its domain.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | inj_typing_imp_le
|
The range of a finite injection is as big as its domain.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | inj_imp_le2
|
The range of a finite injection is as big as its domain.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | pigeon_hole
(Proof Gloss) |
The pigeon-hole principle
A mapping from one finite collection into a smaller collection assigns a single output to two inputs. ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | rel_1_1
|
(![]() ![]() ![]() ![]() ![]() |
def | rel_1_1_b
|
(![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | rel_1_1_eq_rel_1_1_b
|
Equivalence of two forms of relational one-to-one correspondence
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | inv_funs_2
|
(![]() ![]() |
THM | inv_funs_2_identity
|
|
def | one_one_corr_2
|
(types ![]() ![]() ![]() ![]() ![]() |
THM | one_one_corr_2_functionality_wrt_eq
|
![]() ![]() ![]() ![]() |
THM | fun_with_inv2_is_inj
(Proof Gloss) |
![]() ![]() |
THM | fun_with_inv2_is_surj
(Proof Gloss) |
![]() ![]() |
THM | sq_stable__inv_funs_2
|
![]() ![]() ![]() ![]() ![]() |
def | compose_iter
|
Iterated self-composition of a function.
![]() ![]() ![]() ![]() |
def | least
|
(the least number ![]() ![]() ![]() |
THM | least_characterized
|
Characterization of "least".
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() (least i: ![]() ![]() ![]() ![]() ![]() ![]() |
THM | least_characterized2
|
Characterization of "least".
![]() ![]() ![]() ![]() ![]() ![]() ![]() (least i: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | least_satisfies
|
The least number having a property has it.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | least_is_least
|
No number smaller than the least one having a property has it.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | least_is_least2
|
No number smaller than the least one having a property has it.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | least_satisfies2
|
The least number having a property has it.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_discr_range_surj
|
![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ({a:A| ![]() ![]() ![]() (& f ![]() ![]() ![]() ![]() ![]() ![]() (& Surj( ![]() ![]() ![]() |
THM | nsub_discr_range_surjtype
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_inj_discr_range_bij
|
![]() ![]() ( ![]() ![]() ![]() ![]() ({a:A| ![]() ![]() ![]() (& f ![]() ![]() ![]() ![]() ![]() ![]() (& Bij( ![]() ![]() ![]() |
THM | nsub_inj_discr_range_bijtype
|
Characterizing an injection as a bijection
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_surj_least_preimage_total_gen
|
Computing the inverse of a finite function
![]() ![]() ![]() ![]() ![]() ![]() IsEqFun(B;e) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_surj_least_preimage_total
|
Computing the inverse of a finite function
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_surj_least_preimage_works_gen
|
![]() ![]() ![]() ![]() ![]() ![]() IsEqFun(B;e) ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_surj_least_preimage_works
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | find_first_iter
|
== if p(a) ![]() (recursive) |
THM | fin_plus_nat_ooc_nat
|
![]() ![]() ![]() ![]() ![]() |
THM | nat_plus_ooc_nat
|
There are as many positive numbers as non-negative.
![]() ![]() ![]() |
def | is_finite_type
|
![]() ![]() ![]() |
THM | nsub_is_finite
|
![]() ![]() ![]() |
THM | ooc_preserves_finiteness
|
![]() ![]() ![]() ![]() |
THM | no_finite_model_lemma
|
![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | no_finite_model
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | simple_card_cross_assoc
|
![]() ![]() ![]() ![]() |
THM | bijtype_ooc_inj_isect_surjtype
|
![]() ![]() ![]() ![]() |
THM | ifthenelse_distr_subtype_ooc
|
![]() ![]() |
THM | card_subset_vs_and
|
|
THM | card_sum_family_singleton_vs_intseg
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card1_iff_inhabited_uniquely
|
![]() ![]() ![]() ![]() ![]() |
THM | card_void_dom_fun_unit
|
![]() ![]() ![]() ![]() |
THM | nsub_delete
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_delete_rw
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_nsub_inj_vs_lopped
|
The cardinality of injections on a finite nonempty domain in terms of injections on a domain one smaller.
The number ways to order ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_prod_family_singleton_elim
|
![]() ![]() |
THM | card_prod_family_intseg_singleton_elim
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | subset_sq_remove_card
|
![]() |
THM | one_one_corr_2_weakening_wrt
|
![]() ![]() |
THM | card0_iff_uninhabited
|
A class has zero members just when it doesn't have any.
![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_sum_family_singleton_elim
|
![]() ![]() ![]() ![]() |
THM | card_sum_family_intseg_singleton_elim
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | one_one_corr_fams
|
One-to-one correspondence between index families of classes.
== ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() == InvFuns(A;A';f;g) & ( ![]() |
THM | one_one_corr_fams_refl
|
|
THM | decidable_vs_unique_nsub2
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | least_exists
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | least_exists2
|
Existence of a least number having a given property.
![]() ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | is_one_one_corr
|
(function ![]() ![]() ![]() |
def | is_permutation
|
|
def | union_to_sigma
|
|
def | sigma_to_union
|
![]() ![]() |
def | inv_pair
|
(the inverse function pairs between ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | inv_pair_iff_ooc
|
![]() ![]() ![]() ![]() ![]() ![]() |
def | fin_enum
|
(the finite enumerations of ![]() ![]() ![]() ![]() ![]() |
THM | factorial_via_intseg_zero
|
![]() ![]() ![]() |
THM | factorial_via_intseg_step
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | factorial_via_intseg_step_rw
|
![]() ![]() ![]() ![]() ![]() ![]() |
def | unboundedly_infinite
|
(one can find any number of members of ![]() ![]() ![]() ![]() ![]() ![]() |
def | productively_infinite
|
(there is an infinite (omega) sequence of distinct members of ![]() ![]() ![]() ![]() |
THM | unboundedly_imp_productively_infinite
|
![]() ![]() |
def | Dedekind_infinite
|
Dedekind's formulation of infinite class
( ![]() ![]() ![]() ![]() ![]() |
THM | ndiff_bound
|
![]() ![]() ![]() |
THM | eq_mem_is_ax
|
![]() |
THM | comp_preserves_inj
|
Composing injections gives an injection.
![]() ![]() ![]() ![]() |
THM | comp_preserves_surj
|
Composing surjections gives a surjection.
![]() ![]() ![]() ![]() |
THM | surjection_type_surjection
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | surjection_type_nsub_surjection
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | inv_pair_functionality_wrt_one_one_corr
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | one_one_corr_fams_trans
|
One-to-one correspondence between indexed families of classes is transitive.
![]() ![]() ![]() ![]() ![]() ![]() ![]() (x:A. B(x)) ~ (x':A'. B'(x')) ![]() ![]() (x':A'. B'(x')) ~ (x'':A''. B''(x'')) ![]() ![]() |
THM | comp_preserves_bij
|
Composing bijections gives a bijection.
![]() ![]() ![]() ![]() |
THM | one_one_corr_rel_vs_invfuns
|
Equivalence of one-one correspondence and existence of inverses
![]() ![]() ![]() ![]() ![]() (1-1-Corr x:A,y:B. R(x;y)) ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() (InvFuns(A;B;f;g) & ( ![]() ![]() ![]() |
THM | card_split_prod_intseg_family_decbl
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | finite_choice
|
Principle of finite choice. The function can be constructed explicitly without appeal to the ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | dep_finite_choice
|
Principle of dependent finite choice. The function can be constructed explicitly without appeal to the ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | inv_funs_2_sym
|
Being mutual inverses is symmetric.
![]() ![]() |
THM | invfuns_are_surj
|
Mutually inverse functions are surjections.
![]() ![]() |
THM | surjection_type_functionality_wrt_ooc
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | one_one_corr_fams_sym
|
![]() ![]() ![]() ![]() ![]() (x:A. B(x)) ~ (x':A'. B'(x')) ![]() ![]() |
THM | fun_with_inv2_is_inj_rev
|
![]() ![]() |
THM | ooc_preserves_dededkind_inf
|
![]() ![]() ![]() ![]() |
THM | invfuns_are_inj
|
Mutually inverse functions are injections.
![]() ![]() |
THM | injection_type_functionality_wrt_ooc
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | fun_with_inv2_is_surj_rev
|
![]() ![]() |
THM | one_one_corr_is_equiv_rel
|
|
THM | iff_weakening_wrt_one_one_corr_2
|
![]() ![]() ![]() ![]() |
THM | inhabited_functionality_wrt_one_one_corr
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | one_one_corr_2_functionality_wrt_one_one_corr
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | one_one_corr_2_reflex
|
|
THM | one_one_corr_2_inversion
|
![]() ![]() |
THM | one_one_corr_2_transitivity
|
![]() ![]() ![]() ![]() |
COM | one_one_corr_via_bijection
| One-to-One Correspondence via Bijection ... |
COM | one_one_corr_and_bij_thm
| One-to-One Correspondence: equivalence of two characterizations. ... |
THM | inv_funs_2_unique
|
A function has at most one inverse.
![]() ![]() ![]() ![]() |
THM | left_inv_of_surj_is_right_inv
|
A function that cancels a surjection is also cancelled by it.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | parallel_conjunct_imp
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | fun_with_inv2_is_bij
(Proof Gloss) |
![]() ![]() |
THM | fun_with_inv2_is_bij_rev
|
![]() ![]() |
THM | comp_id_r_version2
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | comp_id_l_version2
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | comp_assoc_version2
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | eta_conv_version2
|
![]() ![]() ![]() ![]() |
THM | fun_with_inv_is_bij_version2
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | bij_imp_exists_inv_version2
|
Bijections have inverses.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | bij_iff_1_1_corr_version2
|
![]() ![]() ![]() ![]() ![]() |
THM | int_ooc_nat
|
There are as many non-negative integers as integers.
![]() ![]() |
THM | unb_inf_not_fin
|
![]() ![]() ![]() |
THM | infinite_imp_nonfinite
|
![]() ![]() ![]() |
THM | ooc_preserves_unb_inf
|
![]() ![]() ![]() ![]() |
THM | ooc_preserves_infiniteness
|
![]() ![]() ![]() ![]() |
THM | bij_iff_1_1_corr_version2a
|
![]() ![]() ![]() ![]() ![]() |
THM | negnegelim_imp_notfin_imp_unb_inf
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_not_infinite
|
![]() ![]() ![]() ![]() |
THM | absurd_nonfin_imp_unb_inf
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nonfin_eqv_unb_inf_iff_negnegelim
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | absurd_nonfinite_imp_infinite
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | not_nat_occ_natfuns
|
The infinite sequences of numbers cannot be paired one-to-one with the numbers themselves. (Cantor)
![]() ![]() ![]() ![]() ![]() ![]() |
THM | counting_is_unique
(Proof Gloss) |
Any way of counting a finite class produces the same number.
![]() ![]() ![]() ![]() ![]() ![]() |
THM | fin_card_vs_nat_eq
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | nat_not_finite
|
![]() ![]() |
THM | partition_type
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | bij_imp_exists_inv2
|
Bijections have inverses.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | bij_iff_is_1_1_corr
|
Bijections and one-one correspondence functions are the same.
![]() ![]() |
THM | one_one_corr_fams_if_one_one_corr_B
|
![]() ![]() ![]() |
THM | one_one_corr_fams_if_bij_A
|
![]() ![]() ![]() ![]() ![]() |
THM | one_one_corr_fams_indep_if_one_one_corr
|
![]() ![]() ![]() ![]() |
THM | union_functionality_wrt_one_one_corr
|
![]() ![]() ![]() ![]() |
def | seq_nil
|
|
def | seq_cons
|
![]() ![]() |
THM | card_product_swap
|
![]() ![]() |
THM | card_settype
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_settype_sq
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | set_functionality_wrt_one_one_corr_n_pred2
|
![]() ![]() ![]() ![]() ![]() |
THM | set_functionality_wrt_one_one_corr_n_pred
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_sigma
|
![]() ![]() ![]() ![]() |
THM | product_functionality_wrt_one_one_corr_B
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_quotient
|
![]() ![]() |
THM | product_functionality_wrt_one_one_corr
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_split_prod_intseg_family
|
![]() ![]() ![]() ![]() ![]() (i:{a..b ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | union_sigma_inverses
|
![]() ![]() ![]() ![]() |
THM | card_union_swap
|
|
THM | card_union_vs_sigma
|
![]() ![]() ![]() ![]() |
THM | card_split_decbl
|
![]() ![]() ![]() ![]() |
THM | card_sigma_st_dom
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_split_sigma_dom_decbl
|
![]() ![]() ![]() ![]() ![]() ( ![]() ![]() ![]() ((i:A ![]() ![]() ![]() ![]() |
THM | card_nsub0_union
|
![]() |
THM | card_nsub0_union_2
|
![]() |
THM | card_split_decbl_squash
|
![]() ![]() ![]() ![]() ![]() |
THM | card_split_sum_intseg_family
|
![]() ![]() ![]() ![]() ![]() (i:{a..b ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_split_end_sum_intseg_family
|
![]() ![]() ![]() ![]() ![]() a<b ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_pi
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | function_functionality_wrt_one_one_corr_B
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | function_functionality_wrt_one_one_corr
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_curry_simple
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_curry
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_sigma_distr
|
![]() ![]() ![]() ![]() |
THM | intseg_void
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_void
|
![]() |
THM | intseg_shift
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | intseg_shift_by
|
![]() ![]() ![]() ![]() ![]() |
THM | nsub_unit
|
![]() |
THM | nsub_bool
|
![]() ![]() |
THM | nsub_intseg
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_intseg_rw
|
![]() ![]() ![]() ![]() |
THM | intiseg_intseg
|
![]() ![]() ![]() ![]() ![]() |
THM | intiseg_intseg_plus
|
![]() ![]() ![]() ![]() |
THM | nsub_intiseg_rw
|
![]() ![]() ![]() |
THM | intseg_split
|
![]() ![]() ![]() ![]() ![]() |
THM | nsub_add
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_mul
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_mul_rw
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | mul_assoc_from_cross_assoc
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | finite_indep_sum_card
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_inj_factorial2
|
Relevant to permutation counting problems since these injections are the finite permutations.
![]() ![]() ![]() ![]() |
THM | nsub_inj_factorial_tail
|
Relevant to so-called permutation counting problems since these injections are the ways to order ![]() ![]() ![]() ![]() |
THM | nsub_inj_factorial
|
A more direct proof of this fact is in ![]() ![]() ![]() ![]() |
THM | card_pi_vs_nsub_pi
|
The size of the general product space (whose members are functions) of a finite family of finite classes is the integer product of those classes' sizes.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_fun_vs_nsub_exp
|
Corollary to ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | exp_exp_reduce1
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | exp_exp_reduce2
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_curry_simple2
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_add_rw
|
The size of the disjoint union of two finite classes is the sum of those classes' sizes.
![]() ![]() ![]() ![]() ![]() |
THM | card_sigma_vs_nsub_sigma
|
The size of a general sum (whose members are pairs) of a finite family of finite classes is the integer sum of those classes' sizes.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | inv_pair_inv
|
![]() ![]() |
THM | inv_pair_inv2
|
![]() ![]() ![]() ![]() |
def | next_nat_pair
|
How to step from pair to pair exhaustively
![]() ![]() |
THM | next_nat_pair_not_zeroes
|
The zero-zero pair does not succeed any other.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | next_nat_pair_inj
|
![]() ![]() ![]() ![]() ![]() ![]() |
def | prev_nat_pair
|
Reverses ![]() ![]() |
THM | next_nat_pair_vs_prev_nat_pair
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | nat_to_nat_pair
|
(![]() |
THM | nat_to_nat_pair_inj
|
![]() ![]() ![]() ![]() |
THM | nat_to_nat_pair_surj
|
![]() ![]() ![]() ![]() |
THM | nat_to_nat_pair_bij
|
![]() ![]() ![]() ![]() |
THM | card_nat_vs_nat_nat
|
The ordered pairs of natural numbers can be placed in one-to-one correspondence with the natural numbers. (Cantor)
![]() ![]() ![]() ![]() |
THM | card_nat_vs_nat_tuple
|
The ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_nat_vs_nat_tuples
|
The finite nonempty sequences of natural numbers can be placed in one-one correspondence with the natural numbers themselves.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_nat_vs_nat_tuples_all
|
The finite sequences of natural numbers can be placed in one-one correspondence with the natural numbers themselves.
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_zero
|
![]() ![]() ![]() ![]() |
THM | compose_iter_zero_id
|
![]() ![]() ![]() ![]() |
THM | compose_iter_once
|
![]() ![]() ![]() ![]() |
THM | compose_iter_pos
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_point_id
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_pos_comp
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_id
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_sum
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_sum_comp
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_sum_rw
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_sum_comp_rw
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_prod
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_prod2
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_pos2
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_pos_comp2
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_injection
|
Iteration of an injection is an injection.
![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_inj_cycles
|
A finite permutation always cycles back on each argument.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | iter_perm_cycles_uniform
|
Some positive iteration of any finite permutation is the identity function.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | iter_perm_cycles_uniform2
|
Corollary of Some positive iteration of any finite permutation is the identity function. ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_injection2
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_surjection
|
Iteration of a surjection is a surjection.
![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_bijection
|
Iteration of a bijection is a bijection.
![]() ![]() ![]() ![]() ![]() |
THM | compose_iter_inverses
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | dedekind_inf_imp_inf
|
![]() ![]() |
THM | dededing_imp_unb_inf
|
![]() ![]() |
THM | dedekind_imp_nonfin
|
![]() ![]() ![]() |
THM | nsub_surj_imp_a_rev_inj_gen
|
![]() ![]() ![]() ![]() ![]() ![]() IsEqFun(B;e) ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_surj_imp_a_rev_inj
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_bij_least_preimage_inverse
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_surj_imp_a_rev_inj2
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | surj_typing_imp_le
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_inj_exteq_nsub_surj
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_surj_exteq_nsub_bij
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_surj_ooc_nsub_bij
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_inj_exteq_nsub_bij
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_inj_ooc_nsub_bij
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_inj_ooc_nsub_surj
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | nsub_bij_ooc_invpair
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
def | msize
|
The size of a finite multiset.
![]() ![]() |
def | sized_mset
|
(multisets of size ![]() ![]() ![]() ![]() ![]() |
def | boolsize
|
![]() ![]() ![]() ![]() |
def | sized_bool
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_boolset_vs_mset
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_st_vs_msize
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_st_vs_boolsize
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | card_st_sized_bool
|
![]() ![]() ![]() ![]() ![]() ![]() |
def | same_range_sep
|
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
THM | same_range_sep_eqv
|
![]() ![]() |
THM | same_range_sep_inj_eqv
|
![]() |
COM | counting_intro2
| Counting Indirectly - integer ranges. ... |
COM | counting_intro3
| Counting Indirectly - ordered pairs ... |
COM | counting_intro4
| Counting Indirectly - tuples ... |
THM | is_list_mem_split
|
![]() ![]() ![]() ![]() ![]() ![]() |
THM | is_list_mem_null
|
![]() ![]() ![]() ![]() |
def | list_member_type
|
![]() |
THM | chessboard_example
|
![]() ![]() ![]() ![]() ![]() |
COM | counting_intro5
| Counting indirectly - dependent ordered pairs ... |
COM | counting_intro6
|
Counting indirectly - basic forms: dependent pairs (2). |