author | paulson <lp15@cam.ac.uk> |
Thu, 07 Mar 2019 14:08:05 +0000 | |
changeset 69874 | 11065b70407d |
parent 69735 | 8230dca028eb |
child 71096 | ec7cc76e88e5 |
permissions | -rw-r--r-- |
69735
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
1 |
section \<open>Equipollence and Other Relations Connected with Cardinality\<close> |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
2 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
3 |
theory "Equipollence" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
4 |
imports FuncSet |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
5 |
begin |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
6 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
subsection\<open>Eqpoll\<close> |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
9 |
definition eqpoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl "\<approx>" 50) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
10 |
where "eqpoll A B \<equiv> \<exists>f. bij_betw f A B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
11 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
12 |
definition lepoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl "\<lesssim>" 50) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
13 |
where "lepoll A B \<equiv> \<exists>f. inj_on f A \<and> f ` A \<subseteq> B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
14 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
15 |
definition lesspoll :: "'a set \<Rightarrow> 'b set \<Rightarrow> bool" (infixl \<open>\<prec>\<close> 50) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
16 |
where "A \<prec> B == A \<lesssim> B \<and> ~(A \<approx> B)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
17 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
18 |
lemma lepoll_empty_iff_empty [simp]: "A \<lesssim> {} \<longleftrightarrow> A = {}" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
19 |
by (auto simp: lepoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
20 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
21 |
lemma eqpoll_iff_card_of_ordIso: "A \<approx> B \<longleftrightarrow> ordIso2 (card_of A) (card_of B)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
22 |
by (simp add: card_of_ordIso eqpoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
23 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
24 |
lemma eqpoll_finite_iff: "A \<approx> B \<Longrightarrow> finite A \<longleftrightarrow> finite B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
25 |
by (meson bij_betw_finite eqpoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
26 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
27 |
lemma eqpoll_iff_card: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
28 |
assumes "finite A" "finite B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
29 |
shows "A \<approx> B \<longleftrightarrow> card A = card B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
30 |
using assms by (auto simp: bij_betw_iff_card eqpoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
31 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
32 |
lemma lepoll_antisym: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
33 |
assumes "A \<lesssim> B" "B \<lesssim> A" shows "A \<approx> B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
34 |
using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
35 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
36 |
lemma lepoll_trans [trans]: "\<lbrakk>A \<lesssim> B; B \<lesssim> C\<rbrakk> \<Longrightarrow> A \<lesssim> C" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
37 |
apply (clarsimp simp: lepoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
38 |
apply (rename_tac f g) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
39 |
apply (rule_tac x="g \<circ> f" in exI) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
40 |
apply (auto simp: image_subset_iff inj_on_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
41 |
done |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
42 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
43 |
lemma lepoll_trans1 [trans]: "\<lbrakk>A \<approx> B; B \<lesssim> C\<rbrakk> \<Longrightarrow> A \<lesssim> C" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
44 |
by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans ordIso_iff_ordLeq) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
45 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
46 |
lemma lepoll_trans2 [trans]: "\<lbrakk>A \<lesssim> B; B \<approx> C\<rbrakk> \<Longrightarrow> A \<lesssim> C" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
47 |
apply (clarsimp simp: eqpoll_def lepoll_def bij_betw_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
48 |
apply (rename_tac f g) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
49 |
apply (rule_tac x="g \<circ> f" in exI) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
50 |
apply (auto simp: image_subset_iff inj_on_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
51 |
done |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
52 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
53 |
lemma eqpoll_sym: "A \<approx> B \<Longrightarrow> B \<approx> A" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
54 |
unfolding eqpoll_def |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
55 |
using bij_betw_the_inv_into by auto |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
56 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
57 |
lemma eqpoll_trans [trans]: "\<lbrakk>A \<approx> B; B \<approx> C\<rbrakk> \<Longrightarrow> A \<approx> C" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
58 |
unfolding eqpoll_def using bij_betw_trans by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
59 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
60 |
lemma eqpoll_imp_lepoll: "A \<approx> B \<Longrightarrow> A \<lesssim> B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
61 |
unfolding eqpoll_def lepoll_def by (metis bij_betw_def order_refl) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
62 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
63 |
lemma subset_imp_lepoll: "A \<subseteq> B \<Longrightarrow> A \<lesssim> B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
64 |
by (force simp: lepoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
65 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
66 |
lemma lepoll_iff: "A \<lesssim> B \<longleftrightarrow> (\<exists>g. A \<subseteq> g ` B)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
67 |
unfolding lepoll_def |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
68 |
proof safe |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
69 |
fix g assume "A \<subseteq> g ` B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
70 |
then show "\<exists>f. inj_on f A \<and> f ` A \<subseteq> B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
71 |
by (rule_tac x="inv_into B g" in exI) (auto simp: inv_into_into inj_on_inv_into) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
72 |
qed (metis image_mono the_inv_into_onto) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
73 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
74 |
lemma subset_image_lepoll: "B \<subseteq> f ` A \<Longrightarrow> B \<lesssim> A" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
75 |
by (auto simp: lepoll_iff) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
76 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
77 |
lemma image_lepoll: "f ` A \<lesssim> A" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
78 |
by (auto simp: lepoll_iff) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
79 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
80 |
lemma infinite_le_lepoll: "infinite A \<longleftrightarrow> (UNIV::nat set) \<lesssim> A" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
81 |
apply (auto simp: lepoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
82 |
apply (simp add: infinite_countable_subset) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
83 |
using infinite_iff_countable_subset by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
84 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
85 |
lemma bij_betw_iff_bijections: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
86 |
"bij_betw f A B \<longleftrightarrow> (\<exists>g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
87 |
(is "?lhs = ?rhs") |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
88 |
proof |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
89 |
assume L: ?lhs |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
90 |
then show ?rhs |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
91 |
apply (rule_tac x="the_inv_into A f" in exI) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
92 |
apply (auto simp: bij_betw_def f_the_inv_into_f the_inv_into_f_f the_inv_into_into) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
93 |
done |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
94 |
next |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
95 |
assume ?rhs |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
96 |
then show ?lhs |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
97 |
by (auto simp: bij_betw_def inj_on_def image_def; metis) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
98 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
99 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
100 |
lemma eqpoll_iff_bijections: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
101 |
"A \<approx> B \<longleftrightarrow> (\<exists>f g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
102 |
by (auto simp: eqpoll_def bij_betw_iff_bijections) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
103 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
104 |
lemma lepoll_restricted_funspace: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
105 |
"{f. f ` A \<subseteq> B \<and> {x. f x \<noteq> k x} \<subseteq> A \<and> finite {x. f x \<noteq> k x}} \<lesssim> Fpow (A \<times> B)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
106 |
proof - |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
107 |
have *: "\<exists>U \<in> Fpow (A \<times> B). f = (\<lambda>x. if \<exists>y. (x, y) \<in> U then SOME y. (x,y) \<in> U else k x)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
108 |
if "f ` A \<subseteq> B" "{x. f x \<noteq> k x} \<subseteq> A" "finite {x. f x \<noteq> k x}" for f |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
109 |
apply (rule_tac x="(\<lambda>x. (x, f x)) ` {x. f x \<noteq> k x}" in bexI) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
110 |
using that by (auto simp: image_def Fpow_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
111 |
show ?thesis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
112 |
apply (rule subset_image_lepoll [where f = "\<lambda>U x. if \<exists>y. (x,y) \<in> U then @y. (x,y) \<in> U else k x"]) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
113 |
using * by (auto simp: image_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
114 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
115 |
|
69874 | 116 |
lemma singleton_lepoll: "{x} \<lesssim> insert y A" |
117 |
by (force simp: lepoll_def) |
|
118 |
||
119 |
lemma singleton_eqpoll: "{x} \<approx> {y}" |
|
120 |
by (blast intro: lepoll_antisym singleton_lepoll) |
|
121 |
||
122 |
lemma subset_singleton_iff_lepoll: "(\<exists>x. S \<subseteq> {x}) \<longleftrightarrow> S \<lesssim> {()}" |
|
123 |
proof safe |
|
124 |
show "S \<lesssim> {()}" if "S \<subseteq> {x}" for x |
|
125 |
using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2) |
|
126 |
show "\<exists>x. S \<subseteq> {x}" if "S \<lesssim> {()}" |
|
127 |
by (metis (no_types, hide_lams) image_empty image_insert lepoll_iff that) |
|
128 |
qed |
|
129 |
||
130 |
||
69735
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
131 |
subsection\<open>The strict relation\<close> |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
132 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
133 |
lemma lesspoll_not_refl [iff]: "~ (i \<prec> i)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
134 |
by (simp add: lepoll_antisym lesspoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
135 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
136 |
lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
137 |
by (unfold lesspoll_def, blast) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
138 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
139 |
lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B | A \<approx> B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
140 |
using eqpoll_imp_lepoll lesspoll_def by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
141 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
142 |
lemma lesspoll_trans [trans]: "\<lbrakk>X \<prec> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
143 |
by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
144 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
145 |
lemma lesspoll_trans1 [trans]: "\<lbrakk>X \<lesssim> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
146 |
by (meson eqpoll_sym lepoll_antisym lepoll_trans lepoll_trans1 lesspoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
147 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
148 |
lemma lesspoll_trans2 [trans]: "\<lbrakk>X \<prec> Y; Y \<lesssim> Z\<rbrakk> \<Longrightarrow> X \<prec> Z" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
149 |
by (meson eqpoll_imp_lepoll eqpoll_sym lepoll_antisym lepoll_trans lesspoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
150 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
151 |
lemma eq_lesspoll_trans [trans]: "\<lbrakk>X \<approx> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
152 |
using eqpoll_imp_lepoll lesspoll_trans1 by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
153 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
154 |
lemma lesspoll_eq_trans [trans]: "\<lbrakk>X \<prec> Y; Y \<approx> Z\<rbrakk> \<Longrightarrow> X \<prec> Z" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
155 |
using eqpoll_imp_lepoll lesspoll_trans2 by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
156 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
157 |
subsection\<open>Cartesian products\<close> |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
158 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
159 |
lemma PiE_sing_eqpoll_self: "({a} \<rightarrow>\<^sub>E B) \<approx> B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
160 |
proof - |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
161 |
have 1: "x = y" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
162 |
if "x \<in> {a} \<rightarrow>\<^sub>E B" "y \<in> {a} \<rightarrow>\<^sub>E B" "x a = y a" for x y |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
163 |
by (metis IntD2 PiE_def extensionalityI singletonD that) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
164 |
have 2: "x \<in> (\<lambda>h. h a) ` ({a} \<rightarrow>\<^sub>E B)" if "x \<in> B" for x |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
165 |
using that by (rule_tac x="\<lambda>z\<in>{a}. x" in image_eqI) auto |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
166 |
show ?thesis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
167 |
unfolding eqpoll_def bij_betw_def inj_on_def |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
168 |
by (force intro: 1 2) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
169 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
170 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
171 |
lemma lepoll_funcset_right: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
172 |
"B \<lesssim> B' \<Longrightarrow> A \<rightarrow>\<^sub>E B \<lesssim> A \<rightarrow>\<^sub>E B'" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
173 |
apply (auto simp: lepoll_def inj_on_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
174 |
apply (rule_tac x = "\<lambda>g. \<lambda>z \<in> A. f(g z)" in exI) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
175 |
apply (auto simp: fun_eq_iff) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
176 |
apply (metis PiE_E) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
177 |
by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
178 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
179 |
lemma lepoll_funcset_left: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
180 |
assumes "B \<noteq> {}" "A \<lesssim> A'" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
181 |
shows "A \<rightarrow>\<^sub>E B \<lesssim> A' \<rightarrow>\<^sub>E B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
182 |
proof - |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
183 |
obtain b where "b \<in> B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
184 |
using assms by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
185 |
obtain f where "inj_on f A" and fim: "f ` A \<subseteq> A'" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
186 |
using assms by (auto simp: lepoll_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
187 |
then obtain h where h: "\<And>x. x \<in> A \<Longrightarrow> h (f x) = x" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
188 |
using the_inv_into_f_f by fastforce |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
189 |
let ?F = "\<lambda>g. \<lambda>u \<in> A'. if h u \<in> A then g(h u) else b" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
190 |
show ?thesis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
191 |
unfolding lepoll_def inj_on_def |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
192 |
proof (intro exI conjI ballI impI ext) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
193 |
fix k l x |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
194 |
assume k: "k \<in> A \<rightarrow>\<^sub>E B" and l: "l \<in> A \<rightarrow>\<^sub>E B" and "?F k = ?F l" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
195 |
then have "?F k (f x) = ?F l (f x)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
196 |
by simp |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
197 |
then show "k x = l x" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
198 |
apply (auto simp: h split: if_split_asm) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
199 |
apply (metis PiE_arb h k l) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
200 |
apply (metis (full_types) PiE_E h k l) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
201 |
using fim k l by fastforce |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
202 |
next |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
203 |
show "?F ` (A \<rightarrow>\<^sub>E B) \<subseteq> A' \<rightarrow>\<^sub>E B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
204 |
using \<open>b \<in> B\<close> by force |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
205 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
206 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
207 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
208 |
lemma lepoll_funcset: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
209 |
"\<lbrakk>B \<noteq> {}; A \<lesssim> A'; B \<lesssim> B'\<rbrakk> \<Longrightarrow> A \<rightarrow>\<^sub>E B \<lesssim> A' \<rightarrow>\<^sub>E B'" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
210 |
by (rule lepoll_trans [OF lepoll_funcset_right lepoll_funcset_left]) auto |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
211 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
212 |
lemma lepoll_PiE: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
213 |
assumes "\<And>i. i \<in> A \<Longrightarrow> B i \<lesssim> C i" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
214 |
shows "PiE A B \<lesssim> PiE A C" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
215 |
proof - |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
216 |
obtain f where f: "\<And>i. i \<in> A \<Longrightarrow> inj_on (f i) (B i) \<and> (f i) ` B i \<subseteq> C i" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
217 |
using assms unfolding lepoll_def by metis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
218 |
then show ?thesis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
219 |
unfolding lepoll_def |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
220 |
apply (rule_tac x = "\<lambda>g. \<lambda>i \<in> A. f i (g i)" in exI) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
221 |
apply (auto simp: inj_on_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
222 |
apply (rule PiE_ext, auto) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
223 |
apply (metis (full_types) PiE_mem restrict_apply') |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
224 |
by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
225 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
226 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
227 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
228 |
lemma card_le_PiE_subindex: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
229 |
assumes "A \<subseteq> A'" "Pi\<^sub>E A' B \<noteq> {}" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
230 |
shows "PiE A B \<lesssim> PiE A' B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
231 |
proof - |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
232 |
have "\<And>x. x \<in> A' \<Longrightarrow> \<exists>y. y \<in> B x" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
233 |
using assms by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
234 |
then obtain g where g: "\<And>x. x \<in> A' \<Longrightarrow> g x \<in> B x" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
235 |
by metis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
236 |
let ?F = "\<lambda>f x. if x \<in> A then f x else if x \<in> A' then g x else undefined" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
237 |
have "Pi\<^sub>E A B \<subseteq> (\<lambda>f. restrict f A) ` Pi\<^sub>E A' B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
238 |
proof |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
239 |
show "f \<in> Pi\<^sub>E A B \<Longrightarrow> f \<in> (\<lambda>f. restrict f A) ` Pi\<^sub>E A' B" for f |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
240 |
using \<open>A \<subseteq> A'\<close> |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
241 |
by (rule_tac x="?F f" in image_eqI) (auto simp: g fun_eq_iff) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
242 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
243 |
then have "Pi\<^sub>E A B \<lesssim> (\<lambda>f. \<lambda>i \<in> A. f i) ` Pi\<^sub>E A' B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
244 |
by (simp add: subset_imp_lepoll) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
245 |
also have "\<dots> \<lesssim> PiE A' B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
246 |
by (rule image_lepoll) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
247 |
finally show ?thesis . |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
248 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
249 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
250 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
251 |
lemma finite_restricted_funspace: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
252 |
assumes "finite A" "finite B" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
253 |
shows "finite {f. f ` A \<subseteq> B \<and> {x. f x \<noteq> k x} \<subseteq> A}" (is "finite ?F") |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
254 |
proof (rule finite_subset) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
255 |
show "finite ((\<lambda>U x. if \<exists>y. (x,y) \<in> U then @y. (x,y) \<in> U else k x) ` Pow(A \<times> B))" (is "finite ?G") |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
256 |
using assms by auto |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
257 |
show "?F \<subseteq> ?G" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
258 |
proof |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
259 |
fix f |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
260 |
assume "f \<in> ?F" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
261 |
then show "f \<in> ?G" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
262 |
by (rule_tac x="(\<lambda>x. (x,f x)) ` {x. f x \<noteq> k x}" in image_eqI) (auto simp: fun_eq_iff image_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
263 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
264 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
265 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
266 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
267 |
proposition finite_PiE_iff: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
268 |
"finite(PiE I S) \<longleftrightarrow> PiE I S = {} \<or> finite {i \<in> I. ~(\<exists>a. S i \<subseteq> {a})} \<and> (\<forall>i \<in> I. finite(S i))" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
269 |
(is "?lhs = ?rhs") |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
270 |
proof (cases "PiE I S = {}") |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
271 |
case False |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
272 |
define J where "J \<equiv> {i \<in> I. \<nexists>a. S i \<subseteq> {a}}" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
273 |
show ?thesis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
274 |
proof |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
275 |
assume L: ?lhs |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
276 |
have "infinite (Pi\<^sub>E I S)" if "infinite J" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
277 |
proof - |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
278 |
have "(UNIV::nat set) \<lesssim> (UNIV::(nat\<Rightarrow>bool) set)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
279 |
proof - |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
280 |
have "\<forall>N::nat set. inj_on (=) N" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
281 |
by (simp add: inj_on_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
282 |
then show ?thesis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
283 |
by (meson infinite_iff_countable_subset infinite_le_lepoll top.extremum) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
284 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
285 |
also have "\<dots> = (UNIV::nat set) \<rightarrow>\<^sub>E (UNIV::bool set)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
286 |
by auto |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
287 |
also have "\<dots> \<lesssim> J \<rightarrow>\<^sub>E (UNIV::bool set)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
288 |
apply (rule lepoll_funcset_left) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
289 |
using infinite_le_lepoll that by auto |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
290 |
also have "\<dots> \<lesssim> Pi\<^sub>E J S" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
291 |
proof - |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
292 |
have *: "(UNIV::bool set) \<lesssim> S i" if "i \<in> I" and "\<forall>a. \<not> S i \<subseteq> {a}" for i |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
293 |
proof - |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
294 |
obtain a b where "{a,b} \<subseteq> S i" "a \<noteq> b" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
295 |
by (metis \<open>\<forall>a. \<not> S i \<subseteq> {a}\<close> all_not_in_conv empty_subsetI insertCI insert_subset set_eq_subset subsetI) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
296 |
then show ?thesis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
297 |
apply (clarsimp simp: lepoll_def inj_on_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
298 |
apply (rule_tac x="\<lambda>x. if x then a else b" in exI, auto) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
299 |
done |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
300 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
301 |
show ?thesis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
302 |
by (auto simp: * J_def intro: lepoll_PiE) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
303 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
304 |
also have "\<dots> \<lesssim> Pi\<^sub>E I S" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
305 |
using False by (auto simp: J_def intro: card_le_PiE_subindex) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
306 |
finally have "(UNIV::nat set) \<lesssim> Pi\<^sub>E I S" . |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
307 |
then show ?thesis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
308 |
by (simp add: infinite_le_lepoll) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
309 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
310 |
moreover have "finite (S i)" if "i \<in> I" for i |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
311 |
proof (rule finite_subset) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
312 |
obtain f where f: "f \<in> PiE I S" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
313 |
using False by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
314 |
show "S i \<subseteq> (\<lambda>f. f i) ` Pi\<^sub>E I S" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
315 |
proof |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
316 |
show "s \<in> (\<lambda>f. f i) ` Pi\<^sub>E I S" if "s \<in> S i" for s |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
317 |
using that f \<open>i \<in> I\<close> |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
318 |
by (rule_tac x="\<lambda>j. if j = i then s else f j" in image_eqI) auto |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
319 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
320 |
next |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
321 |
show "finite ((\<lambda>x. x i) ` Pi\<^sub>E I S)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
322 |
using L by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
323 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
324 |
ultimately show ?rhs |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
325 |
using L |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
326 |
by (auto simp: J_def False) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
327 |
next |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
328 |
assume R: ?rhs |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
329 |
have "\<forall>i \<in> I - J. \<exists>a. S i = {a}" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
330 |
using False J_def by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
331 |
then obtain a where a: "\<forall>i \<in> I - J. S i = {a i}" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
332 |
by metis |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
333 |
let ?F = "{f. f ` J \<subseteq> (\<Union>i \<in> J. S i) \<and> {i. f i \<noteq> (if i \<in> I then a i else undefined)} \<subseteq> J}" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
334 |
have *: "finite (Pi\<^sub>E I S)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
335 |
if "finite J" and "\<forall>i\<in>I. finite (S i)" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
336 |
proof (rule finite_subset) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
337 |
show "Pi\<^sub>E I S \<subseteq> ?F" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
338 |
apply safe |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
339 |
using J_def apply blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
340 |
by (metis DiffI PiE_E a singletonD) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
341 |
show "finite ?F" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
342 |
proof (rule finite_restricted_funspace [OF \<open>finite J\<close>]) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
343 |
show "finite (\<Union> (S ` J))" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
344 |
using that J_def by blast |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
345 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
346 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
347 |
show ?lhs |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
348 |
using R by (auto simp: * J_def) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
349 |
qed |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
350 |
qed auto |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
351 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
352 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
353 |
corollary finite_funcset_iff: |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
354 |
"finite(I \<rightarrow>\<^sub>E S) \<longleftrightarrow> (\<exists>a. S \<subseteq> {a}) \<or> I = {} \<or> finite I \<and> finite S" |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
355 |
apply (auto simp: finite_PiE_iff PiE_eq_empty_iff dest: not_finite_existsD) |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
356 |
using finite.simps by auto |
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
357 |
|
8230dca028eb
the theory of Equipollence, and moving Fpow from Cardinals into Main
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
358 |
end |