1 (* ========================================================================= *)
2 (* Cantor's theorem. *)
3 (* ========================================================================= *)
5 (* ------------------------------------------------------------------------- *)
6 (* Ad hoc version for whole type. *)
7 (* ------------------------------------------------------------------------- *)
9 let CANTOR_THM_INJ = prove
10 (`~(?f:(A->bool)->A. (!x y. f(x) = f(y) ==> x = y))`,
11 REWRITE_TAC[INJECTIVE_LEFT_INVERSE; NOT_EXISTS_THM] THEN
12 MAP_EVERY X_GEN_TAC [`f:(A->bool)->A`; `g:A->(A->bool)`] THEN
13 DISCH_THEN(MP_TAC o SPEC `\x:A. ~(g x x)`) THEN MESON_TAC[]);;
15 let CANTOR_THM_SURJ = prove
16 (`~(?f:A->(A->bool). !s. ?x. f x = s)`,
17 REWRITE_TAC[SURJECTIVE_RIGHT_INVERSE; NOT_EXISTS_THM] THEN
18 MAP_EVERY X_GEN_TAC [`g:A->(A->bool)`; `f:(A->bool)->A`] THEN
19 DISCH_THEN(MP_TAC o SPEC `\x:A. ~(g x x)`) THEN MESON_TAC[]);;
21 (* ------------------------------------------------------------------------- *)
22 (* Proper version for any set, in terms of cardinality operators. *)
23 (* ------------------------------------------------------------------------- *)
26 (`!s:A->bool. s <_c {t | t SUBSET s}`,
27 GEN_TAC THEN REWRITE_TAC[lt_c] THEN CONJ_TAC THENL
28 [REWRITE_TAC[le_c] THEN EXISTS_TAC `(=):A->A->bool` THEN
29 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM; SUBSET; IN] THEN MESON_TAC[];
30 REWRITE_TAC[LE_C; IN_ELIM_THM; SURJECTIVE_RIGHT_INVERSE] THEN
31 REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `g:A->(A->bool)` THEN
32 DISCH_THEN(MP_TAC o SPEC `\x:A. s(x) /\ ~(g x x)`) THEN
33 REWRITE_TAC[SUBSET; IN; FUN_EQ_THM] THEN MESON_TAC[]]);;
35 (* ------------------------------------------------------------------------- *)
36 (* More explicit "injective" version as in Paul Taylor's book. *)
37 (* ------------------------------------------------------------------------- *)
39 let CANTOR_THM_INJ' = prove
40 (`~(?f:(A->bool)->A. (!x y. f(x) = f(y) ==> x = y))`,
42 ABBREV_TAC `(g:A->A->bool) = \a. { b | !s. f(s) = a ==> b IN s}` THEN
43 MP_TAC(ISPEC `g:A->A->bool`
44 (REWRITE_RULE[NOT_EXISTS_THM] CANTOR_THM_SURJ)) THEN
45 FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
46 ASM_REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
49 (* ------------------------------------------------------------------------- *)
50 (* Another sequence of versions (Lawvere, Cantor, Taylor) taken from *)
51 (* http://ncatlab.org/nlab/show/Cantor%27s+theorem. *)
52 (* ------------------------------------------------------------------------- *)
54 let CANTOR_LAWVERE = prove
56 (!f:A->B. ?x:A. h(x) = f) ==> !n:B->B. ?x. n(x) = x`,
58 ABBREV_TAC `g:A->B = \a. (n:B->B) (h a a)` THEN
59 RULE_ASSUM_TAC(REWRITE_RULE[FUN_EQ_THM]) THEN
63 (`!f:A->(A->bool). ~(!s. ?x. f x = s)`,
64 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP CANTOR_LAWVERE) THEN
65 DISCH_THEN(MP_TAC o SPEC `(~)`) THEN MESON_TAC[]);;
67 let CANTOR_TAYLOR = prove
68 (`!f:(A->bool)->A. ~(!x y. f(x) = f(y) ==> x = y)`,
70 MP_TAC(ISPEC `\a:A. { b:A | !s. f(s) = a ==> b IN s}`
71 (REWRITE_RULE[NOT_EXISTS_THM] CANTOR)) THEN
72 REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
75 let SURJECTIVE_COMPOSE = prove
76 (`(!y. ?x. f(x) = y) /\ (!z. ?y. g(y) = z)
77 ==> (!z. ?x. (g o f) x = z)`,
80 let INJECTIVE_SURJECTIVE_PREIMAGE = prove
81 (`!f:A->B. (!x y. f(x) = f(y) ==> x = y) ==> !t. ?s. {x | f(x) IN s} = t`,
83 EXISTS_TAC `IMAGE (f:A->B) t` THEN
84 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE] THEN
87 let CANTOR_JOHNSTONE = prove
88 (`!i:B->S f:B->S->bool.
89 ~((!x y. i(x) = i(y) ==> x = y) /\ (!s. ?z. f(z) = s))`,
92 `(IMAGE (f:B->S->bool)) o (\s:S->bool. {x | i(x) IN s})`
93 (REWRITE_RULE[NOT_EXISTS_THM] CANTOR)) THEN
94 REWRITE_TAC[] THEN MATCH_MP_TAC SURJECTIVE_COMPOSE THEN
95 ASM_REWRITE_TAC[SURJECTIVE_IMAGE] THEN
96 MATCH_MP_TAC INJECTIVE_SURJECTIVE_PREIMAGE THEN