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)) |