Selected Objects
| Introduction | Introductory Remarks |
| def | is_one_one_corr_rel
|
One-one correlation as a relation
1-1-Corr x:A,y:B. R(x;y) == ( x:A.  !y:B. R(x;y)) & (y:B. !x:A. R(x;y)) |
| def | is_list_mem
|
(a is a member of list xs)
a  xs == Case of xs; nil  False ; x.ys a = x A  (a ys) (recursive) |
| THM | ndiff_vs_diff
|
a,b: . a b   (b -- a) = b-a |
| THM | eq_int_is_eq_nsub
|
IsEqFun( b;  i,j. i=j) |
| THM | decidable__nat_equal
|
i,j:. Dec(i = j) |
| THM | exteq_singleton_vs_intseg
|
a,a':. a'-a = 1 ({a..a' } =ext {a:}) |
| THM | exteq_prod_family_singleton_vs_intseg
|
a,a':.
a'-a = 1 (B:({a..a'}  Type{i}). (i:{a..a'}B(i)) =ext ({a:}B(a))) |
| THM | exteq_sum_family_singleton_vs_intseg
|
a,a':.
a'-a = 1 (B:({a..a'}Type{i}). (i:{a..a'} B(i)) =ext ({a:}B(a))) |
| def | injection_type
|
(the injections from A into B)
A inj B == {f:(AB)| Inj(A; B; f) } |
| def | bijection_type
|
(the bijections from A onto B)
A bij B == {f:(AB)| Bij(A; B; f) } |
| THM | injtype_vs_inj
|
((A inj B))  (f:(AB). Inj(A; B; f)) |
| THM | injection_type_fun
|
f:(A inj B). f AB |
| THM | injection_type_injection
|
f:(A inj B). Inj(A; B; f) |
| THM | inj_point_deletion
|
f:(A inj B), a:A. f {x:A|  x = a }{y:B| y = f(a) } |
| THM | inj_point_deletion_inj
|
f:(A inj B), a:A. f {x:A| x = a } inj {y:B| y = f(a) } |
| THM | inj_from_empty_unique
|
(A) (!(A inj B)) |
| THM | bijtype_sub_injtype
|
(A bij B)  (A inj B) |
| THM | bijection_type_inc_inj
|
(A bij B) (A inj B) |
| THM | nsub_inj_lop_typing
|
a: , b:, f:(a inj b). f (a-1) inj {x:b| x = f(a-1) } |
| THM | nsub_inj_fill_typing
|
a:, b:, j:b, f:((a-1) inj {x:b| x = j }).
(i.if i=a-1 j else f(i) fi) a inj b |
| def | surjection_type
|
(the surjections from A onto B)
A onto B == {f:(AB)| Surj(A; B; f) } |
| THM | bijtype_sub_surjtype
|
(A bij B) (A onto B) |
| THM | bijection_type_inc_surj
|
(A bij B) (A onto B) |
| THM | bijtype_exteq_inj_isect_surjtype
|
(A bij B) =ext ((A inj B) (A onto B)) |
| COM | unicomp_assoc
|
 h o g o f = h o g o f
... |
| COM | inverse_function_intro
|
Explain inverse functions and
Def InvFuns(A; B; f; g) == g o f = Id & f o g = Id |
| 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
seq:l(i) == l[i] |
| COM | note_on_generalization_for_induction
|
Not done yet. |
| def | replace_fn_values
|
(Replace values x s.t. P(x) by y in f)(i) == if P(f(i)) y else f(i) fi |
| def | delete_fenum_value
|
Special purpose operation for shrinking the domain and range of an injection simultaneously. See REMARK.
Replace value k by f(m) in f == Replace values x s.t. x=k by f(m) in f |
| COM | delete_fenum_value_example
|
 let xs = [1; 3; 0; 7; 2; 4; 6; 5] in
 let v = 4 in (Replace value v by seq:xs(||xs||-1) in seq:xs){(||xs||-1)}
*
[1; 3; 0; 7; 2; 5; 6] |
| THM | delete_fenum_value_comp1_gen
|
Inj({u:| P(u) }; {u:| Q(u) }; f)
(m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }.
(f(i) = k (Replace value k by f(m) in f)(i) = f(m) {v:| Q(v) & v = k }) |
| THM | delete_fenum_value_comp2_gen
|
Inj({u:| P(u) }; {u:| Q(u) }; f)
(m:{u:| P(u) }, k:{v:| Q(v) }, i:{u:| P(u) & u = m }.
(f(i) = k (Replace value k by f(m) in f)(i) = f(i) {v:| Q(v) & v = k }) |
| THM | delete_fenum_value_is_inj_genW
|
Inj({u:| P(u) }; {v:| Q(v) }; f)
(m:{u:| P(u) }, k:{v:| Q(v) }.
((Replace value k by f(m) in f) {u:| P(u) & u = m }{v:| Q(v) & v = k }
(& Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
(& Inj(Replace value k by f(m) in f)) |
| THM | delete_fenum_value_is_inj_gen
|
Inj({u:| P(u) }; {v:| Q(v) }; f)
(m:{u:| P(u) }, k:{v:| Q(v) }.
(Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
(Inj(Replace value k by f(m) in f)) |
| THM | delete_fenum_value_is_fenum_gen
|
Bij({u:| P(u) }; {v:| Q(v) }; f)
(m:{u:| P(u) }, k:{v:| Q(v) }.
(Bij({u:| P(u) & u = m }; {v:| Q(v) & v = k };
(Bij(Replace value k by f(m) in f)) |
| THM | delete_fenum_value_comp1
|
Inj((m+1); (k+1); f)
(i:m. f(i) = k (Replace value k by f(m) in f)(i) = f(m) k) |
| THM | delete_fenum_value_comp2
|
Inj((m+1); (k+1); f)
(i:m. f(i) = k (Replace value k by f(m) in f)(i) = f(i) k) |
| THM | delete_fenum_value_is_inj
|
Inj((m+1); (k+1); f) Inj(m; k; Replace value k by f(m) in f) |
| THM | delete_fenum_value_is_fenum
|
Bij((m+1); (k+1); f) Bij(m; k; Replace value k by f(m) in f) |
| THM | finite_inj_counter_example
(Proof Gloss) |
Lemma for the pigeon-hole principle.
A finite non-injection into integers maps some two distinct arguments to the same value.
m:, f:(m). Inj(m; ; f) (x:m, y:x. f(x) = f(y)) |
| THM | inj_imp_le
(Proof Gloss) |
The range of a finite injection is as big as its domain.
(f:(mk). Inj(m; k; f)) mk |
| THM | inj_typing_imp_le
|
The range of a finite injection is as big as its domain.
((m inj k)) mk |
| THM | inj_imp_le2
|
The range of a finite injection is as big as its domain.
m,k:, f:(mk). Inj(m; k; f) mk |
| 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.
m,k:, f:(mk). k<m (x,y:m. x  y & f(x) = f(y)) |
| def | rel_1_1
|
(R is a 1-1 relation)
R is 1-1 == x,x':A, y,y':B. R(x,y) & R(x',y') (x = x' y = y') |
| def | rel_1_1_b
|
(R(x;y) is a 1-1 relation in x in A and y in B)
1-1 xA,yB. R(x;y) == x,x':A, y,y':B. R(x;y) & R(x';y') (x = x' y = y') |
| THM | rel_1_1_eq_rel_1_1_b
|
Equivalence of two forms of relational one-to-one correspondence
R:(ABProp). (R is 1-1) = (1-1 xA,yB. R(x;y)) |
| def | inv_funs_2
|
(f and g are inverse functions, i.e. they cancel each other)
InvFuns(A;B;f;g) == (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y) |
| THM | inv_funs_2_identity
|
InvFuns(A;A;Id;Id) |
| def | one_one_corr_2
|
(types A and B are in one-to-one corresponence)
A ~ B == f:(AB), g:(BA). InvFuns(A;B;f;g) |
| THM | one_one_corr_2_functionality_wrt_eq
|
A = A' B = B' (A ~ B) = (A' ~ B') |
| THM | fun_with_inv2_is_inj
(Proof Gloss) |
InvFuns(A;B;f;g) Inj(A; B; f) |
| THM | fun_with_inv2_is_surj
(Proof Gloss) |
InvFuns(A;B;f;g) Surj(A; B; f) |
| THM | sq_stable__inv_funs_2
|
f:(AB), g:(BA). SqStable(InvFuns(A;B;f;g)) |
| def | compose_iter
|
Iterated self-composition of a function.
f{ i}(x) == if i=0 x else f(f{i-1}(x)) fi (recursive) |
| def | least
|
(the least number i such that p(i))
least i:. p(i) == if p(0) 0 else (least i:. p(i+1))+1 fi (recursive) |
| THM | least_characterized
|
Characterization of "least".
k:, p:{p:(k )| i:k. p(i) }.
(least i:. p(i)) {i:k| p(i) & (j:i. p(j)) } |
| THM | least_characterized2
|
Characterization of "least".
p:{p:()| i:. p(i) }.
(least i:. p(i)) {i:| p(i) & (j:. j<i p(j)) } |
| THM | least_satisfies
|
The least number having a property has it.
k:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i)) |
| THM | least_is_least
|
No number smaller than the least one having a property has it.
k:, p:{p:(k)| i:k. p(i) }, j:(least i:. p(i)). p(j) |
| THM | least_is_least2
|
No number smaller than the least one having a property has it.
p:{p:()| i:. p(i) }, j:(least i:. p(i)). p(j) |
| THM | least_satisfies2
|
The least number having a property has it.
p:{p:()| i:. p(i) }. p(least i:. p(i)) |
| THM | nsub_discr_range_surj
|
(A Discrete)
(k:, f:(kA).
({a:A| i:k. a = f(i) } Type
(& f k{a:A| i:k. a = f(i) }
(& Surj(k; {a:A| i:k. a = f(i) }; f)) |
| THM | nsub_discr_range_surjtype
|
(A Discrete) (k:, f:(kA). f k onto {a:A| i:k. a = f(i) }) |
| THM | nsub_inj_discr_range_bij
|
(A Discrete)
(k:, f:(k inj A).
({a:A| i:k. a = f(i) } Type
(& f k{a:A| i:k. a = f(i) }
(& Bij(k; {a:A| i:k. a = f(i) }; f)) |
| THM | nsub_inj_discr_range_bijtype
|
Characterizing an injection as a bijection
(A Discrete) (k:, f:(k inj A). f k bij {a:A| i:k. a = f(i) }) |
| THM | nsub_surj_least_preimage_total_gen
|
Computing the inverse of a finite function
e:(BB).
IsEqFun(B;e) (a:, f:(a onto B), y:B. (least x:. (f(x)) e y) a) |
| THM | nsub_surj_least_preimage_total
|
Computing the inverse of a finite function
f:(a onto b), y:b. (least x:. f(x)=y) a |
| THM | nsub_surj_least_preimage_works_gen
|
e:(BB).
IsEqFun(B;e) (a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y) |
| THM | nsub_surj_least_preimage_works
|
f:(a onto b), y:b. f(least x:. f(x)=y) = y |
| def | find_first_iter
|
find_first_iter(v.p(v); v.f(v); a)
== if p(a) a else find_first_iter(v.p(v); v.f(v); f(a)) fi
(recursive) |
| THM | fin_plus_nat_ooc_nat
|
k:. (k+) ~ |
| THM | nat_plus_ooc_nat
|
There are as many positive numbers as non-negative.
~ |
| def | is_finite_type
|
Finite(A) == n:. A ~ n |
| THM | nsub_is_finite
|
k:. Finite(k) |
| THM | ooc_preserves_finiteness
|
(A ~ B) Finite(A) Finite(B) |
| THM | no_finite_model_lemma
|
R:(AAProp).
(A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y))
(k:. f:(kA). i,j:k. i<j R(f(i);f(j))) |
| THM | no_finite_model
|
(A:Type, R:(AAProp).
((A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y))
(& (x:A. R(x;x))
(& Finite(A)) |
| THM | simple_card_cross_assoc
|
(ABC) ~ ((AB)C) |
| THM | bijtype_ooc_inj_isect_surjtype
|
(A bij B) ~ ((A inj B)(A onto B)) |
| THM | ifthenelse_distr_subtype_ooc
|
{x:A| if b P(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi |
| THM | card_subset_vs_and
|
{x:{x:A| P(x) }| Q(x) } ~ {x:A| P(x) & Q(x) } |
| THM | card_sum_family_singleton_vs_intseg
|
a,a':. a'-a = 1 (B:({a..a'}Type{i}). (i:{a..a'}B(i)) ~ ({a:}B(a))) |
| THM | card1_iff_inhabited_uniquely
|
(A ~ 1) (!A) |
| THM | card_void_dom_fun_unit
|
(0A) ~ 1 |
| THM | nsub_delete
|
k:, j:k, m:. m = k-1 ({i:k| i = j } ~ m) |
| THM | nsub_delete_rw
|
k:, j:k. {i:k| i = j } ~ (k-1) |
| 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 a distinct objects from among b is b times the number of ways to order a-1 distinct objects from among b-1.
a,b:. (a inj b) ~ (b((a-1) inj (b-1))) |
| THM | card_prod_family_singleton_elim
|
(i:{a:A}B(i)) ~ B(a) |
| THM | card_prod_family_intseg_singleton_elim
|
a,a':. a'-a = 1 (B:({a..a'}Type{i}). (i:{a..a'}B(i)) ~ B(a)) |
| THM | subset_sq_remove_card
|
{x:A|  B(x) } ~ {x:A| B(x) } |
| THM | one_one_corr_2_weakening_wrt
|
A = B (A ~ B) |
| THM | card0_iff_uninhabited
|
A class has zero members just when it doesn't have any.
(A ~ 0) (A) |
| THM | card_sum_family_singleton_elim
|
B:({a:A}Type). (i:{a:A}B(i)) ~ B(a) |
| THM | card_sum_family_intseg_singleton_elim
|
a,a':. a'-a = 1 (B:({a..a'}Type{i}). (i:{a..a'}B(i)) ~ B(a)) |
| def | one_one_corr_fams
|
One-to-one correspondence between index families of classes.
(x:A. B(x)) ~ (x':A'. B'(x'))
== f:(AA'), g:(A'A), F:(x:AB(x)B'(f(x))), G:(x:AB'(f(x))B(x)).
== InvFuns(A;A';f;g) & (u:A. InvFuns(B(u);B'(f(u));F(u);G(u))) |
| THM | one_one_corr_fams_refl
|
(x:A. B(x)) ~ (x:A. B(x)) |
| THM | decidable_vs_unique_nsub2
|
Dec(P) (!i:2. if i=0 P else P fi) |
| THM | least_exists
|
k:, P:{P:(kProp)| i:k. P(i) }.
(i:k. Dec(P(i))) ({i:k| P(i) & (j:i. P(j)) }) |
| THM | least_exists2
|
Existence of a least number having a given property.
P:{P:(Prop)| i:. P(i) }.
(i:. Dec(P(i))) ({i:| P(i) & (j:. j<i P(j)) }) |
| def | is_one_one_corr
|
(function f is a one-to-one correspondence)
f is 1-1 corr == g:(BA). InvFuns(A;B;f;g) |
| def | is_permutation
|
f is permutation on A == f is 1-1 corr |
| def | union_to_sigma
|
union_to_sigma(e) == InjCase(e; a. <0,a>; b. <1,b>) |
| def | sigma_to_union
|
sigma_to_union(e) == e/i,u. if i=0 inl(u) else inr(u) fi |
| def | inv_pair
|
(the inverse function pairs between A and B)
A B == {fg:((AB)(BA))| fg/f,g. InvFuns(A;B;f;g) } |
| THM | inv_pair_iff_ooc
|
((AB)) (A ~ B) |
| def | fin_enum
|
(the finite enumerations of A)
fin_enum(A) == k:kA |
| THM | factorial_via_intseg_zero
|
0! |
| THM | factorial_via_intseg_step
|
k,n:. k = n+1 k! = k n! |
| THM | factorial_via_intseg_step_rw
|
k:. k! = k(k-1)! |
| def | unboundedly_infinite
|
(one can find any number of members of A)
Unbounded(A) == k:. (k inj A) |
| def | productively_infinite
|
(there is an infinite (omega) sequence of distinct members of A)
Infinite(A) == ( inj A) |
| THM | unboundedly_imp_productively_infinite
|
Infinite(A) Unbounded(A) |
| def | Dedekind_infinite
|
Dedekind's formulation of infinite class
(A can be mapped 1-1 into a proper subpart of itself)
Dedekind-Infinite(A) == a:A, f:(AA). Inj(A; A; f) & (x:A. f(x) = a) |
| THM | ndiff_bound
|
b,a:. b(b -- a)+a |
| THM | eq_mem_is_ax
|
a,a':A, x:(a = a'). x = * |
| THM | comp_preserves_inj
|
Composing injections gives an injection.
Inj(A; B; g) Inj(B; C; f) Inj(A; C; f o g) |
| THM | comp_preserves_surj
|
Composing surjections gives a surjection.
Surj(A; B; g) Surj(B; C; f) Surj(A; C; f o g) |
| THM | surjection_type_surjection
|
f:(A onto B), a:. a onto A (B Discrete) Surj(A; B; f) |
| THM | surjection_type_nsub_surjection
|
f:(a onto b). Surj(a; b; f) |
| THM | inv_pair_functionality_wrt_one_one_corr
|
(A ~ A') (B ~ B') ((AB) ~ (A'B')) |
| THM | one_one_corr_fams_trans
|
One-to-one correspondence between indexed families of classes is transitive.
A:Type, A',A'':Type, B:(AType), B':(A'Type), B'':(A''Type).
(x:A. B(x)) ~ (x':A'. B'(x'))
(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.
Bij(A; B; g) Bij(B; C; f) Bij(A; C; f o g) |
| THM | one_one_corr_rel_vs_invfuns
|
Equivalence of one-one correspondence and existence of inverses
R:(ABProp).
(1-1-Corr x:A,y:B. R(x;y))
(f:(AB), g:(BA).
(InvFuns(A;B;f;g) & (x:A, y:B. R(x;y) y = f(x) & x = g(y))) |
| THM | card_split_prod_intseg_family_decbl
|
(x:A. Dec(P(x))) ((x:AB(x)) ~ ((x:A st P(x)B(x))(x:A st P(x)B(x)))) |
| THM | finite_choice
|
Principle of finite choice. The function can be constructed explicitly without appeal to the Axiom of Choice.
k:, Q:(kAProp). (x:k. y:A. Q(x;y)) (f:(kA). x:k. Q(x;f(x))) |
| THM | dep_finite_choice
|
Principle of dependent finite choice. The function can be constructed explicitly without appeal to the Dependent Axiom of Choice.
k:, B:(kType), Q:(x:kB(x)Prop).
(x:k. y:B(x). Q(x;y)) (f:(x:kB(x)). x:k. Q(x;f(x))) |
| THM | inv_funs_2_sym
|
Being mutual inverses is symmetric.
InvFuns(A;B;f;g) InvFuns(B;A;g;f) |
| THM | invfuns_are_surj
|
Mutually inverse functions are surjections.
InvFuns(A;B;f;g) Surj(A; B; f) & Surj(B; A; g) |
| THM | surjection_type_functionality_wrt_ooc
|
(A ~ A') (B ~ B') ((A onto B) ~ (A' onto B')) |
| THM | one_one_corr_fams_sym
|
B:(AType), B':(A'Type).
(x:A. B(x)) ~ (x':A'. B'(x')) (x':A'. B'(x')) ~ (x:A. B(x)) |
| THM | fun_with_inv2_is_inj_rev
|
InvFuns(A;B;f;g) Inj(B; A; g) |
| THM | ooc_preserves_dededkind_inf
|
(A ~ B) Dedekind-Infinite(A) Dedekind-Infinite(B) |
| THM | invfuns_are_inj
|
Mutually inverse functions are injections.
InvFuns(A;B;f;g) Inj(A; B; f) & Inj(B; A; g) |
| THM | injection_type_functionality_wrt_ooc
|
(A ~ A') (B ~ B') ((A inj B) ~ (A' inj B')) |
| THM | fun_with_inv2_is_surj_rev
|
InvFuns(A;B;f;g) Surj(B; A; g) |
| THM | one_one_corr_is_equiv_rel
|
EquivRel X,Y:Type. X ~ Y |
| THM | iff_weakening_wrt_one_one_corr_2
|
(A ~ B) (A B) |
| THM | inhabited_functionality_wrt_one_one_corr
|
(A ~ B) ((A) (B)) |
| THM | one_one_corr_2_functionality_wrt_one_one_corr
|
(A ~ A') (B ~ B') ((A ~ B) (A' ~ B')) |
| THM | one_one_corr_2_reflex
|
A ~ A |
| THM | one_one_corr_2_inversion
|
(A ~ B) (B ~ A) |
| THM | one_one_corr_2_transitivity
|
(A ~ B) (B ~ C) (A ~ C) |
| 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.
InvFuns(A;B;f;g) InvFuns(A;B;f;h) g = h |
| THM | left_inv_of_surj_is_right_inv
|
A function that cancels a surjection is also cancelled by it.
g:(BA). Surj(A; B; f) (x:A. g(f(x)) = x) (y:B. f(g(y)) = y) |
| THM | parallel_conjunct_imp
|
(A C) (B D) A & B C & D |
| THM | fun_with_inv2_is_bij
(Proof Gloss) |
InvFuns(A;B;f;g) Bij(A; B; f) |
| THM | fun_with_inv2_is_bij_rev
|
InvFuns(A;B;f;g) Bij(B; A; g) |
| THM | comp_id_r_version2
|
f:(AB). f o Id = f AB |
| THM | comp_id_l_version2
|
f:(AB). Id o f = f AB |
| THM | comp_assoc_version2
|
f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f AD |
| THM | eta_conv_version2
|
f:(AB). (x.f(x)) = f |
| THM | fun_with_inv_is_bij_version2
|
f:(AB), g:(BA). InvFuns(A;B;f;g) Bij(A; B; f) |
| THM | bij_imp_exists_inv_version2
|
Bijections have inverses.
f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A;B;f;g)) |
| THM | bij_iff_1_1_corr_version2
|
(f:(AB). Bij(A; B; f)) (A ~ B) |
| THM | int_ooc_nat
|
There are as many non-negative integers as integers.
~ |
| THM | unb_inf_not_fin
|
Unbounded(A) Finite(A) |
| THM | infinite_imp_nonfinite
|
Infinite(A) Finite(A) |
| THM | ooc_preserves_unb_inf
|
(A ~ B) Unbounded(A) Unbounded(B) |
| THM | ooc_preserves_infiniteness
|
(A ~ B) Infinite(A) Infinite(B) |
| THM | bij_iff_1_1_corr_version2a
|
(f:(AB). Bij(A; B; f)) (B ~ A) |
| THM | negnegelim_imp_notfin_imp_unb_inf
|
(P:Prop. P P) (A:Type. Finite(A) Unbounded(A)) |
| THM | nsub_not_infinite
|
k:. Infinite(k) |
| THM | absurd_nonfin_imp_unb_inf
|
(A:Type. Finite(A) Unbounded(A)) (D:Type. (D) (D)) |
| THM | nonfin_eqv_unb_inf_iff_negnegelim
|
(A:Type. Finite(A) Unbounded(A)) (P:Prop. P P) |
| THM | absurd_nonfinite_imp_infinite
|
(A:Type. Finite(A) Infinite(A)) (D:Type. (D) (D)) |
| 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.
(A ~ m) (A ~ k) m = k |
| THM | fin_card_vs_nat_eq
|
a,b:. (a ~ b) a = b |
| THM | nat_not_finite
|
Finite() |
| THM | partition_type
|
P:(ABProp). (x:A. !y:B. P(x;y)) (A ~ (y:B{x:A| P(x;y) })) |
| THM | bij_imp_exists_inv2
|
Bijections have inverses.
f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A;B;f;g)) |
| THM | bij_iff_is_1_1_corr
|
Bijections and one-one correspondence functions are the same.
Bij(A; B; f) f is 1-1 corr |
| THM | one_one_corr_fams_if_one_one_corr_B
|
(x:A. B(x) ~ B'(x)) (x:A. B(x)) ~ (x:A. B'(x)) |
| THM | one_one_corr_fams_if_bij_A
|
g:(A'A). Bij(A'; A; g) (x:A. B(x)) ~ (x':A'. B(g(x'))) |
| THM | one_one_corr_fams_indep_if_one_one_corr
|
(A ~ A') (B ~ B') (:A. B) ~ (:A'. B') |
| THM | union_functionality_wrt_one_one_corr
|
(A ~ A') (B ~ B') ((A+B) ~ (A'+B')) |
| def | seq_nil
|
Nil(i) == i |
| def | seq_cons
|
[x/ xs](i) == if i=0 x else xs(i-1) fi |
| THM | card_product_swap
|
(AB) ~ (BA) |
| THM | card_settype
|
Bij(A; A'; f) (x:A. B(x) B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) }) |
| THM | card_settype_sq
|
Bij(A; A'; f) (x:A. B(x) B'(f(x))) ({x:A| B(x) } ~ {x:A'| B'(x) }) |
| THM | set_functionality_wrt_one_one_corr_n_pred2
|
(x:A. B(x) B'(x)) ({x:A| B(x) } ~ {x:A| B'(x) }) |
| THM | set_functionality_wrt_one_one_corr_n_pred
|
(x:A. B(x) B'(x)) ({x:A| B(x) } ~ {x:A| B'(x) }) |
| THM | card_sigma
|
(x:A. B(x)) ~ (x:A'. B'(x)) ((x:AB(x)) ~ (x:A'B'(x))) |
| THM | product_functionality_wrt_one_one_corr_B
|
B,B':(AType). (x:A. B(x) ~ B'(x)) ((x:AB(x)) ~ (x:AB'(x))) |
| THM | card_quotient
|
(q:A/E{x:A| q = x A/E }) ~ A |
| THM | product_functionality_wrt_one_one_corr
|
(A ~ A') (B ~ B') ((AB) ~ (A'B')) |
| THM | card_split_prod_intseg_family
|
a,b:, c:{a...b}, B:({a..b}Type).
(i:{a..b}B(i)) ~ ((i:{a..c}B(i))(i:{c..b}B(i))) |
| THM | union_sigma_inverses
|
InvFuns(A+B;i:2if i=0 A else B fi;union_to_sigma;sigma_to_union) |
| THM | card_union_swap
|
(A+B) ~ (B+A) |
| THM | card_union_vs_sigma
|
(A+B) ~ (i:2if i=0 A else B fi) |
| THM | card_split_decbl
|
(x:A. Dec(P(x))) (A ~ ({x:A| P(x) }+{x:A| P(x) })) |
| THM | card_sigma_st_dom
|
B:(AType), P:(AProp). (i:{i:A| P(i) }B(i)) ~ {v:(i:AB(i))| P(v/x,y. x) } |
| THM | card_split_sigma_dom_decbl
|
B:(AType), P:(AProp).
(i:A. Dec(P(i)))
((i:AB(i)) ~ ((i:{i:A| P(i) }B(i))+(i:{i:A| P(i) }B(i)))) |
| THM | card_nsub0_union
|
(0+A) ~ A |
| THM | card_nsub0_union_2
|
(A+0) ~ A |
| THM | card_split_decbl_squash
|
(x:A. Dec(P(x))) (A ~ ({x:A| P(x) }+{x:A| P(x) })) |
| THM | card_split_sum_intseg_family
|
a,b:, c:{a...b}, B:({a..b}Type).
(i:{a..b}B(i)) ~ ((i:{a..c}B(i))+(i:{c..b}B(i))) |
| THM | card_split_end_sum_intseg_family
|
a,b:, B:({a..b}Type).
a<b ((i:{a..b}B(i)) ~ ((i:{a..(b-1)}B(i))+B(b-1))) |
| THM | card_pi
|
(x:A. B(x)) ~ (x:A'. B'(x)) ((x:AB(x)) ~ (x:A'B'(x))) |
| THM | function_functionality_wrt_one_one_corr_B
|
B,B':(AType). (x:A. B(x) ~ B'(x)) ((x:AB(x)) ~ (x:AB'(x))) |
| THM | function_functionality_wrt_one_one_corr
|
(A ~ A') (B ~ B') ((AB) ~ (A'B')) |
| THM | card_curry_simple
|
(ABC) ~ (ABC) |
| THM | card_curry
|
(z:(x:AB(x))C(z)) ~ (x:Ay:B(x)C(<x,y>)) |
| THM | card_sigma_distr
|
(xy:(x:AB(x))C(xy)) ~ (x:Ay:B(x)C(<x,y>)) |
| THM | intseg_void
|
a,b:. ba (Void ~ {a..b}) |
| THM | nsub_void
|
Void ~ 0 |
| THM | intseg_shift
|
a,b,a',b':. b-a = b'-a' ({a..b} ~ {a'..b'}) |
| THM | intseg_shift_by
|
a:, b,c:. {a..b} ~ {(a+c)..(b+c)} |
| THM | nsub_unit
|
Unit ~ 1 |
| THM | nsub_bool
|
~ 2 |
| THM | nsub_intseg
|
c,a:, b:. c = b-a ({a..b} ~ c) |
| THM | nsub_intseg_rw
|
a,b:. {a..b} ~ (b-a) |
| THM | intiseg_intseg
|
a,b',b:. b = b'+1 ({a...b'} ~ {a..b}) |
| THM | intiseg_intseg_plus
|
a:, b:. {a...b} ~ {a..(b+1)} |
| THM | nsub_intiseg_rw
|
a,b:. {a...b} ~ (1+b-a) |
| THM | intseg_split
|
a,b:, c:{a...b}. ({a..c}+{c..b}) ~ {a..b} |
| THM | nsub_add
|
c,a,b:. a+b = c ((a+b) ~ c) |
| THM | nsub_mul
|
a,b,c:. ab = c ((ab) ~ c) |
| THM | nsub_mul_rw
|
a,b:. (ab) ~ (ab) |
| THM | mul_assoc_from_cross_assoc
|
a,b,c:. a(bc) = (ab)c |
| THM | finite_indep_sum_card
|
a,b:. (A ~ a) (B ~ b) ((AB) ~ (ab)) |
| THM | nsub_inj_factorial2
|
Relevant to permutation counting problems since these injections are the finite permutations.
(b inj b) ~ (b!) |
| THM | nsub_inj_factorial_tail
|
Relevant to so-called permutation counting problems since these injections are the ways to order a distinct values chosen from a total of b values.
(a inj b) ~ (b!a) |
| THM | nsub_inj_factorial
|
A more direct proof of this fact is in nsub inj factorial2.
(k inj k) ~ (k!) |
| 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.
a:, b:(a). (i:ab(i)) ~ ( i:a. b(i)) |
| THM | card_fun_vs_nsub_exp
|
Corollary to card pi vs nsub pi
a,b:. (ab) ~ (b a) |
| THM | exp_exp_reduce1
|
a,b,c:. c(ab) = (cb)a |
| THM | exp_exp_reduce2
|
a,b,c:. c(ab) = (ca)b |
| THM | card_curry_simple2
|
(ABC) ~ (BAC) |
| THM | nsub_add_rw
|
The size of the disjoint union of two finite classes is the sum of those classes' sizes.
a,b:. (a+b) ~ (a+b) |
| 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.
a:, b:(a). (i:ab(i)) ~ ( i:a. b(i)) |
| THM | inv_pair_inv
|
(AB) ~ (A ~ B) |
| THM | inv_pair_inv2
|
((AB)) ~ (A ~ B) |
| def | next_nat_pair
|
How to step from pair to pair exhaustively
next_nat_pair(xy) == xy/x,y. if y=0 <0,x+1> else <x+1,y-1> fi |
| THM | next_nat_pair_not_zeroes
|
The zero-zero pair does not succeed any other.
xy:(). <0,0> = next_nat_pair(xy) |
| THM | next_nat_pair_inj
|
Inj(; ; next_nat_pair) |
| def | prev_nat_pair
|
Reverses next nat pair
prev_nat_pair(xy) == xy/x,y. if x=0 <y-1,0> else <x-1,y+1> fi |
| THM | next_nat_pair_vs_prev_nat_pair
|
InvFuns(;{xy:()| xy = <0,0> };next_nat_pair;prev_nat_pair) |
| def | nat_to_nat_pair
|
(i steps of next_nat_pair from <0,0>)
nat_to_nat_pair(i) == next_nat_pair{i}(<0,0>) |
| THM | nat_to_nat_pair_inj
|
Inj(; ; nat_to_nat_pair) |
| THM | nat_to_nat_pair_surj
|
Surj(; ; nat_to_nat_pair) |
| THM | nat_to_nat_pair_bij
|
Bij(; ; nat_to_nat_pair) |
| 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 k-tuples of natural numbers can be placed in one-to-one correspondence with the natural numbers theselves.
k:. (k) ~ |
| 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.
(k:k) ~ |
| 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.
(k:k) ~ |
| THM | compose_iter_zero
|
f:(AA), x:A. f{0}(x) = x |
| THM | compose_iter_zero_id
|
f:(AA). f{0} = Id |
| THM | compose_iter_once
|
f:(AA). f{1} = f |
| THM | compose_iter_pos
|
f:(AA), i:, x:A. f{i}(x) = f(f{i-1}(x)) |
| THM | compose_iter_point_id
|
f:(AA), u:A. f(u) = u (i:. f{i}(u) = u) |
| THM | compose_iter_pos_comp
|
f:(AA), i:. f{i} = f o f{i-1} |
| THM | compose_iter_id
|
i:. Id{i} = Id AA |
| THM | compose_iter_sum
|
x:A, f:(AA), i,j,k:. k = i+j f{i}(f{j}(x)) = f{k}(x) |
| THM | compose_iter_sum_comp
|
f:(AA), i,j,k:. k = i+j f{i} o f{j} = f{k} |
| THM | compose_iter_sum_rw
|
x:A, f:(AA), k:, i:{0...k}. f{k}(x) = f{i}(f{k-i}(x)) |
| THM | compose_iter_sum_comp_rw
|
f:(AA), k:, i:{0...k}. f{k} = f{i} o f{k-i} |
| THM | compose_iter_prod
|
x:A, f:(AA), i,j,k:. k = ij f{i}{j}(x) = f{k}(x) A |
| THM | compose_iter_prod2
|
x:A, f:(AA), i,j:. f{i}{j}(x) = f{ij}(x) |
| THM | compose_iter_pos2
|
f:(AA), i:, x:A. f{i}(x) = f{i-1}(f(x)) |
| THM | compose_iter_pos_comp2
|
f:(AA), i:. f{i} = f{i-1} o f |
| THM | compose_iter_injection
|
Iteration of an injection is an injection.
Inj(A; A; f) (i:. Inj(A; A; f{i})) |
| THM | compose_iter_inj_cycles
|
A finite permutation always cycles back on each argument.
k:, f:(k inj k), u:k. i:. f{i}(u) = u |
| THM | iter_perm_cycles_uniform
|
Some positive iteration of any finite permutation is the identity function.
k:, f:(k inj k). i:. u:k. f{i}(u) = u |
| THM | iter_perm_cycles_uniform2
|
Corollary of iter perm cycles uniform.
Some positive iteration of any finite permutation is the identity function.
k:, f:(k inj k). i:. f{i} = Id kk |
| THM | compose_iter_injection2
|
f:(A inj A), i:. f{i} A inj A |
| THM | compose_iter_surjection
|
Iteration of a surjection is a surjection.
Surj(A; A; f) (i:. Surj(A; A; f{i})) |
| THM | compose_iter_bijection
|
Iteration of a bijection is a bijection.
Bij(A; A; f) (i:. Bij(A; A; f{i})) |
| THM | compose_iter_inverses
|
InvFuns(A;A;f;g) (i:. InvFuns(A;A;f{i};g{i})) |
| THM | dedekind_inf_imp_inf
|
Dedekind-Infinite(A) Infinite(A) |
| THM | dededing_imp_unb_inf
|
Dedekind-Infinite(A) Unbounded(A) |
| THM | dedekind_imp_nonfin
|
Dedekind-Infinite(A) Finite(A) |
| THM | nsub_surj_imp_a_rev_inj_gen
|
e:(BB).
IsEqFun(B;e) (a:, f:(a onto B). (y.least x:. (f(x)) e y) B inj a) |
| THM | nsub_surj_imp_a_rev_inj
|
f:(a onto b). (y.least x:. f(x)=y) b inj a |
| THM | nsub_bij_least_preimage_inverse
|
f:(a bij a). InvFuns(a;a;f;y.least x:. f(x)=y) |
| THM | nsub_surj_imp_a_rev_inj2
|
((a onto b)) ((b inj a)) |
| THM | surj_typing_imp_le
|
((a onto b)) ba |
| THM | nsub_inj_exteq_nsub_surj
|
(k inj k) =ext (k onto k) |
| THM | nsub_surj_exteq_nsub_bij
|
(k onto k) =ext (k bij k) |
| THM | nsub_surj_ooc_nsub_bij
|
(k onto k) ~ (k bij k) |
| THM | nsub_inj_exteq_nsub_bij
|
(k inj k) =ext (k bij k) |
| THM | nsub_inj_ooc_nsub_bij
|
(k inj k) ~ (k bij k) |
| THM | nsub_inj_ooc_nsub_surj
|
(k inj k) ~ (k onto k) |
| THM | nsub_bij_ooc_invpair
|
(a bij a) ~ (aa) |
| def | msize
|
The size of a finite multiset.
Msize(f) == i:k. f(i) |
| def | sized_mset
|
(multisets of size k)
a {k} T == {p:(aT)| Msize(p) = k } |
| def | boolsize
|
size(a)(p) == Msize(x.if p(x) 1 else 0 fi) |
| def | sized_bool
|
a {k} == {p:(a)| size(a)(p) = k } |
| THM | card_boolset_vs_mset
|
(a {k} ) ~ (a {k} 2) |
| THM | card_st_vs_msize
|
f:(a2). (i:a. P(i) f(i) = 1 2) ({x:a| P(x) } ~ (Msize(f))) |
| THM | card_st_vs_boolsize
|
p:(a). {x:a| p(x) } ~ (size(a)(p)) |
| THM | card_st_sized_bool
|
p:(a {k} ). {i:a| p(i) } ~ k |
| def | same_range_sep
|
same_range_sep(A; B) == f,g. j:B. (i:A. f(i) = j) (i:A. g(i) = j) |
| THM | same_range_sep_eqv
|
EquivRel on AB, same_range_sep(A; B) |
| THM | same_range_sep_inj_eqv
|
EquivRel on A inj B, same_range_sep(A; B) |
| 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
|
x,a:A, ys:A List. (x a.ys) x = a (x ys) |
| THM | is_list_mem_null
|
x:A. (x nil) False |
| def | list_member_type
|
xs == {a:A| a xs } |
| THM | chessboard_example
|
(AH ~ 8) ((AH{1...8}) ~ 64) |
| COM | counting_intro5
|
Counting indirectly - dependent ordered pairs
... |
| COM | counting_intro6
|
Counting indirectly - basic forms: dependent pairs (2). Counting(dependent pairs - 1)
... |