theory Cardinal_ZF imports ZF.CardinalArith func1
begin
This theory file deals with results on cardinal numbers (cardinals). Cardinals are a genaralization of the natural numbers, used to measure the cardinality (size) of sets. Contributed by Daniel de la Concepcion.
Some new ideas on cardinals
All the results of this section are done without assuming the Axiom of Choice. With the Axiom of Choice in play, the proofs become easier and some of the assumptions may be dropped.
Since General Topology Theory is closely related to Set Theory, it is very interesting to make use of all the possibilities of Set Theory to try to classify homeomorphic topological spaces. These ideas are generally used to prove that two topological spaces are not homeomorphic.
There exist cardinals which are the successor of another cardinal, but; as happens with ordinals, there are cardinals which are limit cardinal.
definition
\( \text{LimitC}(i) \equiv \text{Card}(i) \wedge 0 \lt i \wedge (\forall y.\ (y \lt i\wedge \text{Card}(y)) \longrightarrow \text{csucc}(y) \lt i) \)
Simple fact used a couple of times in proofs.
lemma nat_less_infty:
assumes \( n\in nat \) and \( \text{InfCard}(X) \)
shows \( n \lt X \)proof from assms have \( n \lt nat \) and \( nat\leq X \) using lt_def, InfCard_def
then show \( n \lt X \) using lt_trans2
qed
There are three types of cardinals, the zero one, the succesors of other cardinals and the limit cardinals.
lemma Card_cases_disj:
assumes \( \text{Card}(i) \)
shows \( i=0 | (\exists j.\ \text{Card}(j) \wedge i=\text{csucc}(j)) | \text{LimitC}(i) \)proof from assms have D: \( Ord(i) \) using Card_is_Ord
{
assume F: \( i\neq 0 \)
assume Contr: \( ~ \text{LimitC}(i) \)
from F, D have \( 0 \lt i \) using Ord_0_lt
with Contr, assms have \( \exists y.\ y \lt i \wedge \text{Card}(y) \wedge \neg \text{csucc}(y) \lt i \) using LimitC_def
then obtain \( y \) where \( y \lt i \wedge \text{Card}(y) \wedge \neg \text{csucc}(y) \lt i \)
with D have \( y \lt i \), \( i\leq \text{csucc}(y) \) and O: \( \text{Card}(y) \) using not_lt_imp_le, lt_Ord, Card_csucc, Card_is_Ord
with assms have \( \text{csucc}(y)\leq i \), \( i\leq \text{csucc}(y) \) using csucc_le
then have \( i=\text{csucc}(y) \) using le_anti_sym
with O have \( \exists j.\ \text{Card}(j) \wedge i=\text{csucc}(j) \)
thus \( thesis \)
qed
Given an ordinal bounded by a cardinal in ordinal order, we can change to the order of sets.
lemma le_imp_lesspoll:
assumes \( \text{Card}(Q) \)
shows \( A \leq Q \Longrightarrow A \preceq Q \)proof assume \( A \leq Q \)
then have \( A \lt Q\vee A=Q \) using le_iff
then have \( A\approx Q\vee A \lt Q \) using eqpoll_refl
with assms have \( A\approx Q\vee A\prec Q \) using lt_Card_imp_lesspoll
then show \( A\preceq Q \) using lesspoll_def, eqpoll_imp_lepoll
qed
There are two types of infinite cardinals, the natural numbers and those that have at least one infinite strictly smaller cardinal.
lemma InfCard_cases_disj:
assumes \( \text{InfCard}(Q) \)
shows \( Q=nat \vee (\exists j.\ \text{csucc}(j)\preceq Q \wedge \text{InfCard}(j)) \)proof{
}
assume \( \forall j.\ \neg \text{csucc}(j) \preceq Q \vee \neg \text{InfCard}(j) \)
then have D: \( \neg \text{csucc}(nat) \preceq Q \) using InfCard_nat
with D, assms have \( \neg (\text{csucc}(nat) \leq Q) \) using le_imp_lesspoll, InfCard_is_Card
with assms have \( Q \lt (\text{csucc}(nat)) \) using not_le_iff_lt, Card_is_Ord, Card_csucc, Card_is_Ord, Card_is_Ord, InfCard_is_Card, Card_nat
with assms have \( Q\leq nat \) using Card_lt_csucc_iff, InfCard_is_Card, Card_nat
with assms have \( Q=nat \) using InfCard_def, le_anti_sym
thus \( thesis \)
qed
A more readable version of standard Isabelle/ZF Ord_linear_lt
lemma Ord_linear_lt_IML:
assumes \( Ord(i) \), \( Ord(j) \)
shows \( i \lt j \vee i=j \vee j \lt i \) using assms, lt_def, Ord_linear, disjEA set is injective and not bijective to the successor of a cardinal if and only if it is injective and possibly bijective to the cardinal.
lemma Card_less_csucc_eq_le:
assumes \( \text{Card}(m) \)
shows \( A \prec \text{csucc}(m) \longleftrightarrow A \preceq m \)proof have S: \( Ord(\text{csucc}(m)) \) using Card_csucc, Card_is_Ord, assms
{
assume A: \( A \prec \text{csucc}(m) \)
with S have \( |A|\approx A \) using lesspoll_imp_eqpoll
also
from A have \( \ldots \prec \text{csucc}(m) \)
finally have \( |A|\prec \text{csucc}(m) \)
then have \( |A|\preceq \text{csucc}(m) \), \( ~(|A|\approx \text{csucc}(m)) \) using lesspoll_def
with S have \( ||A||\leq \text{csucc}(m) \), \( |A|\neq \text{csucc}(m) \) using lepoll_cardinal_le
then have \( |A|\leq \text{csucc}(m) \), \( |A|\neq \text{csucc}(m) \) using Card_def, Card_cardinal
then have I: \( ~(\text{csucc}(m) \lt |A|) \), \( |A|\neq \text{csucc}(m) \) using le_imp_not_lt
from S have \( \text{csucc}(m) \lt |A| \vee |A|=\text{csucc}(m) \vee |A| \lt \text{csucc}(m) \) using Card_cardinal, Card_is_Ord, Ord_linear_lt_IML
with I have \( |A| \lt \text{csucc}(m) \)
with assms have \( |A|\leq m \) using Card_lt_csucc_iff, Card_cardinal
then have \( |A|=m\vee |A| \lt m \) using le_iff
then have \( |A|\approx m\vee |A| \lt m \) using eqpoll_refl
then have \( |A|\approx m\vee |A|\prec m \) using lt_Card_imp_lesspoll, assms
then have T: \( |A|\preceq m \) using lesspoll_def, eqpoll_imp_lepoll
from A, S have \( A\approx |A| \) using lesspoll_imp_eqpoll, eqpoll_sym
also
from T have \( \ldots \preceq m \)
finally show \( A\preceq m \)
assume A: \( A\preceq m \)
from assms have \( m\prec \text{csucc}(m) \) using lt_Card_imp_lesspoll, Card_csucc, Card_is_Ord, lt_csucc
with A show \( A\prec \text{csucc}(m) \) using lesspoll_trans1
If the successor of a cardinal is infinite, so is the original cardinal.
lemma csucc_inf_imp_inf:
assumes \( \text{Card}(j) \) and \( \text{InfCard}(\text{csucc}(j)) \)
shows \( \text{InfCard}(j) \)proof{
}
assume f: \( Finite (j) \)
then obtain \( n \) where \( n\in nat \), \( j\approx n \) using Finite_def
with assms(1) have TT: \( j=n \), \( n\in nat \) using cardinal_cong, nat_into_Card, Card_def
then have Q: \( succ(j)\in nat \) using nat_succI
with f, TT have T: \( Finite(succ(j)) \), \( \text{Card}(succ(j)) \) using nat_into_Card, nat_succI
from T(2) have \( \text{Card}(succ(j))\wedge j \lt succ(j) \) using Card_is_Ord
moreover
}
}
ultimately have \( (\ \lt mu> L.\ \text{Card}(L) \wedge j \lt L)=succ(j) \) by (rule Least_equality )
from this have \( Ord(succ(j)) \) using Card_is_Ord
moreover {
fix \( x \)
assume A: \( x \lt succ(j) \)
{
assume \( \text{Card}(x)\wedge j \lt x \)
with A have \( False \) using lt_trans1
hence \( ~(\text{Card}(x)\wedge j \lt x) \)
then have \( \text{csucc}(j)=succ(j) \) using csucc_def
with Q have \( \text{csucc}(j)\in nat \)
then have \( \text{csucc}(j) \lt nat \) using lt_def, Card_nat, Card_is_Ord
with assms(2) have \( False \) using InfCard_def, lt_trans2
then have \( ~(Finite (j)) \)
with assms(1) show \( thesis \) using Inf_Card_is_InfCard
qed
Since all the cardinals previous to nat are finite, it cannot be a successor cardinal; hence it is a LimitC cardinal.
corollary LimitC_nat:
shows \( \text{LimitC}(nat) \)proof note Card_nat
moreover
}
}
ultimately show \( thesis \) using LimitC_def
qed
have \( 0 \lt nat \) using lt_def
moreover {
fix \( y \)
assume AS: \( y \lt nat \), \( \text{Card}(y) \)
then have ord: \( Ord(y) \) unfolding lt_def
then have Cacsucc: \( \text{Card}(\text{csucc}(y)) \) using Card_csucc
{
assume \( nat\leq \text{csucc}(y) \)
with Cacsucc have \( \text{InfCard}(\text{csucc}(y)) \) using InfCard_def
with AS(2) have \( \text{InfCard}(y) \) using csucc_inf_imp_inf
then have \( nat\leq y \) using InfCard_def
with AS(1) have \( False \) using lt_trans2
hence \( ~(nat\leq \text{csucc}(y)) \)
then have \( \text{csucc}(y) \lt nat \) using not_le_iff_lt, Ord_nat, Cacsucc, Card_is_Ord
Main result on cardinals (without the Axiom of Choice)
If two sets are strictly injective to an infinite cardinal, then so is its union. For the case of successor cardinal, this theorem is done in the isabelle library in a more general setting; but that theorem is of not use in the case where \( \text{LimitC}(Q) \) and it also makes use of the Axiom of Choice. The mentioned theorem is in the theory file Cardinal_AC.thy
Note that if \(Q\) is finite and different from \(1\), let's assume \(Q=n\), then the union of \(A\) and \(B\) is not bounded by \(Q\). Counterexample: two disjoint sets of \(n-1\) elements each have a union of \(2n-2\) elements which are more than \(n\).
Note also that if \(Q=1\) then \(A\) and \(B\) must be empty and the union is then empty too; and \(Q\) cannot be 0 because no set is injective and not bijective to 0.
The proof is divided in two parts, first the case when both sets \(A\) and \(B\) are finite; and second, the part when at least one of them is infinite. In the first part, it is used the fact that a finite union of finite sets is finite. In the second part it is used the linear order on cardinals (ordinals). This proof can not be generalized to a setting with an infinite union easily.
lemma less_less_imp_un_less:
assumes \( A\prec Q \) and \( B\prec Q \) and \( \text{InfCard}(Q) \)
shows \( A \cup B\prec Q \)proof{
}
assume \( Finite (A) \wedge Finite(B) \)
then have \( Finite(A \cup B) \) using Finite_Un
then obtain \( n \) where R: \( A \cup B \approx n \), \( n\in nat \) using Finite_def
then have \( |A \cup B| \lt nat \) using lt_def, cardinal_cong, nat_into_Card, Card_def, Card_nat, Card_is_Ord
with assms(3) have T: \( |A \cup B| \lt Q \) using InfCard_def, lt_trans2
from R have \( Ord(n) \), \( A \cup B \preceq n \) using nat_into_Card, Card_is_Ord, eqpoll_imp_lepoll
then have \( A \cup B\approx |A \cup B| \) using lepoll_Ord_imp_eqpoll, eqpoll_sym
also
from T, assms(3) have \( \ldots \prec Q \) using lt_Card_imp_lesspoll, InfCard_is_Card
finally have \( A \cup B\prec Q \)
moreover {
}
}
}
ultimately show \( A \cup B\prec Q \)
qed
assume \( ~(Finite (A) \wedge Finite(B)) \)
hence A: \( ~Finite (A) \vee ~Finite(B) \)
from assms have B: \( |A|\approx A \), \( |B|\approx B \) using lesspoll_imp_eqpoll, lesspoll_imp_eqpoll, InfCard_is_Card, Card_is_Ord
from B(1) have Aeq: \( \forall x.\ (|A|\approx x) \longrightarrow (A\approx x) \) using eqpoll_sym, eqpoll_trans
from B(2) have Beq: \( \forall x.\ (|B|\approx x) \longrightarrow (B\approx x) \) using eqpoll_sym, eqpoll_trans
with A, Aeq have \( ~Finite(|A|)\vee ~Finite(|B|) \) using Finite_def
then have D: \( \text{InfCard}(|A|)\vee \text{InfCard}(|B|) \) using Inf_Card_is_InfCard, Inf_Card_is_InfCard, Card_cardinal
{
assume AS: \( |A| \lt |B| \)
{
assume \( ~\text{InfCard}(|A|) \)
with D have \( \text{InfCard}(|B|) \)
moreover {
}
ultimately have INFB: \( \text{InfCard}(|B|) \)
assume \( \text{InfCard}(|A|) \)
then have \( nat\leq |A| \) using InfCard_def
with AS have \( nat \lt |B| \) using lt_trans1
then have \( nat\leq |B| \) using leI
then have \( \text{InfCard}(|B|) \) using InfCard_def, Card_cardinal
then have \( 2 \lt |B| \) using nat_less_infty
then have AG: \( 2\preceq |B| \) using lt_Card_imp_lesspoll, Card_cardinal, lesspoll_def
from B(2) have \( |B|\approx B \)
also
from assms(2) have \( \ldots \prec Q \)
finally have TTT: \( |B|\prec Q \)
from B(1) have \( \text{Card}(|B|) \), \( A \preceq |A| \) using eqpoll_sym, Card_cardinal, eqpoll_imp_lepoll
with AS have \( A\prec |B| \) using lt_Card_imp_lesspoll, lesspoll_trans1
then have I1: \( A\preceq |B| \) using lesspoll_def
from B(2) have I2: \( B\preceq |B| \) using eqpoll_sym, eqpoll_imp_lepoll
have \( A \cup B\preceq A+B \) using Un_lepoll_sum
also
from I1, I2 have \( \ldots \preceq |B| + |B| \) using sum_lepoll_mono
also from AG have \( \ldots \preceq |B| * |B| \) using sum_lepoll_prod
also from assms(3), INFB have \( \ldots \approx |B| \) using InfCard_square_eqpoll
finally have \( A \cup B\preceq |B| \)
also
from TTT have \( \ldots \prec Q \)
finally have \( A \cup B\prec Q \)
moreover {
}
}
moreover {
}
ultimately have \( A \cup B\prec Q \) using Ord_linear_lt_IML, Card_cardinal, Card_is_Ord
assume AS: \( |B| \lt |A| \)
{
assume \( ~\text{InfCard}(|B|) \)
with D have \( \text{InfCard}(|A|) \)
moreover {
}
ultimately have INFB: \( \text{InfCard}(|A|) \)
assume \( \text{InfCard}(|B|) \)
then have \( nat\leq |B| \) using InfCard_def
with AS have \( nat \lt |A| \) using lt_trans1
then have \( nat\leq |A| \) using leI
then have \( \text{InfCard}(|A|) \) using InfCard_def, Card_cardinal
then have \( 2 \lt |A| \) using nat_less_infty
then have AG: \( 2\preceq |A| \) using lt_Card_imp_lesspoll, Card_cardinal, lesspoll_def
from B(1) have \( |A|\approx A \)
also
from assms(1) have \( \ldots \prec Q \)
finally have TTT: \( |A|\prec Q \)
from B(2) have \( \text{Card}(|A|) \), \( B \preceq |B| \) using eqpoll_sym, Card_cardinal, eqpoll_imp_lepoll
with AS have \( B\prec |A| \) using lt_Card_imp_lesspoll, lesspoll_trans1
then have I1: \( B\preceq |A| \) using lesspoll_def
from B(1) have I2: \( A\preceq |A| \) using eqpoll_sym, eqpoll_imp_lepoll
have \( A \cup B\preceq A+B \) using Un_lepoll_sum
also
from I1, I2 have \( \ldots \preceq |A| + |A| \) using sum_lepoll_mono
also from AG have \( \ldots \preceq |A| * |A| \) using sum_lepoll_prod
also from INFB, assms(3) have \( \ldots \approx |A| \) using InfCard_square_eqpoll
finally have \( A \cup B\preceq |A| \)
also
from TTT have \( \ldots \prec Q \)
finally have \( A \cup B\prec Q \)
assume AS: \( |A|=|B| \)
with D have INFB: \( \text{InfCard}(|A|) \)
then have \( 2 \lt |A| \) using nat_less_infty
then have AG: \( 2\preceq |A| \) using lt_Card_imp_lesspoll, Card_cardinal using lesspoll_def
from B(1) have \( |A|\approx A \)
also
from assms(1) have \( \ldots \prec Q \)
finally have TTT: \( |A|\prec Q \)
from AS, B have I1: \( A\preceq |A| \) and I2: \( B\preceq |A| \) using eqpoll_refl, eqpoll_imp_lepoll, eqpoll_sym
have \( A \cup B\preceq A+B \) using Un_lepoll_sum
also
from I1, I2 have \( \ldots \preceq |A| + |A| \) using sum_lepoll_mono
also from AG have \( \ldots \preceq |A| * |A| \) using sum_lepoll_prod
also from assms(3), INFB have \( \ldots \approx |A| \) using InfCard_square_eqpoll
finally have \( A \cup B\preceq |A| \)
also
from TTT have \( \ldots \prec Q \)
finally have \( A \cup B\prec Q \)
Choice axioms
We want to prove some theorems assuming that some version of the Axiom of Choice holds. To avoid introducing it as an axiom we will define an appropriate predicate and put that in the assumptions of the theorems. That way technically we stay inside ZF.
The first predicate we define states that the axiom of \(Q\)-choice holds for subsets of \(K\) if we can find a choice function for every family of subsets of \(K\) whose (that family's) cardinality does not exceed \(Q\).
definition
\( \text{ the axiom of } Q \text{ choice holds for subsets }K \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0 \wedge Nt\subseteq K)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)
Next we define a general form of \(Q\) choice where we don't require a collection of files to be included in a file.
definition
\( \text{ the axiom of } Q \text{ choice holds } \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)
The axiom of finite choice always holds.
theorem finite_choice:
assumes \( n\in nat \)
shows \( \text{ the axiom of } n \text{ choice holds } \)proof note assms(1)
moreover {
}
}
}
}
ultimately show \( thesis \) by (rule nat_induct )
qed
fix \( M \) \( N \)
assume \( M\preceq 0 \), \( \forall t\in M.\ Nt\neq 0 \)
then have \( M=0 \) using lepoll_0_is_0
then have \( \{\langle t,0\rangle .\ t\in M\}:\text{Pi}(M,\lambda t.\ Nt) \) unfolding Pi_def, domain_def, function_def, Sigma_def
moreover
from \( M=0 \) have \( \forall t\in M.\ \{\langle t,0\rangle .\ t\in M\}t\in Nt \)
ultimately have \( (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt)) \)
then have \( (\forall M N.\ (M \preceq 0 \wedge (\forall t\in M.\ Nt\neq 0)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)
then have \( \text{ the axiom of } 0 \text{ choice holds } \) using AxiomCardinalChoiceGen_def, nat_into_Card
moreover {
fix \( x \)
assume as: \( x\in nat \), \( \text{ the axiom of } x \text{ choice holds } \)
{
fix \( M \) \( N \)
assume ass: \( M\preceq succ(x) \), \( \forall t\in M.\ Nt\neq 0 \)
{
assume \( M\preceq x \)
from as(2), ass(2) have \( (M \preceq x \wedge (\forall t\in M.\ N t \neq 0)) \longrightarrow (\exists f.\ f \in \text{Pi}(M,\lambda t.\ N t) \wedge (\forall t\in M.\ f t \in N t)) \) unfolding AxiomCardinalChoiceGen_def
with \( M\preceq x \), ass(2) have \( (\exists f.\ f \in \text{Pi}(M,\lambda t.\ N t) \wedge (\forall t\in M.\ f t \in N t)) \)
moreover {
}
ultimately have \( \exists g.\ g \in \text{Pi}(M, \lambda t.\ Nt) \wedge (\forall t\in M.\ g t \in N t) \) using as(1), ass(1), lepoll_succ_disj
assume \( M\approx succ(x) \)
then obtain \( f \) where f: \( f\in \text{bij}(succ(x),M) \) using eqpoll_sym, eqpoll_def
moreover
have \( x\in succ(x) \) unfolding succ_def
ultimately have \( \text{restrict}(f,succ(x)-\{x\})\in \text{bij}(succ(x)-\{x\},M-\{fx\}) \) using bij_restrict_rem
moreover
have \( x\notin x \) using mem_not_refl
then have \( succ(x)-\{x\}=x \) unfolding succ_def
ultimately have \( \text{restrict}(f,x)\in \text{bij}(x,M-\{fx\}) \)
then have \( x\approx M-\{fx\} \) unfolding eqpoll_def
then have \( M-\{fx\}\approx x \) using eqpoll_sym
then have \( M-\{fx\}\preceq x \) using eqpoll_imp_lepoll
with as(2), ass(2) have \( (\exists g.\ g \in \text{Pi}(M-\{fx\},\lambda t.\ N t) \wedge (\forall t\in M-\{fx\}.\ g t \in N t)) \) unfolding AxiomCardinalChoiceGen_def
then obtain \( g \) where g: \( g\in \text{Pi}(M-\{fx\},\lambda t.\ N t) \), \( \forall t\in M-\{fx\}.\ g t \in N t \)
from f have ff: \( fx\in M \) using bij_def, inj_def, apply_funtype
with ass(2) have \( N(fx)\neq 0 \)
then obtain \( y \) where y: \( y\in N(fx) \)
from g(1) have gg: \( g\subseteq Sigma(M-\{fx\},()(N)) \) unfolding Pi_def
with y, ff have \( g \cup \{\langle fx, y\rangle \}\subseteq Sigma(M, ()(N)) \) unfolding Sigma_def
moreover
from g(1) have dom: \( M-\{fx\}\subseteq domain(g) \) unfolding Pi_def
then have \( M\subseteq domain(g \cup \{\langle fx, y\rangle \}) \) unfolding domain_def
moreover from gg, g(1) have noe: \( ~(\exists t.\ \langle fx,t\rangle \in g) \) and \( function(g) \) unfolding domain_def, Pi_def, Sigma_def
with dom have fg: \( function(g \cup \{\langle fx, y\rangle \}) \) unfolding function_def
ultimately have PP: \( g \cup \{\langle fx, y\rangle \}\in \text{Pi}(M,\lambda t.\ N t) \) unfolding Pi_def
have \( \langle fx, y\rangle \in g \cup \{\langle fx, y\rangle \} \)
from this, fg have \( (g \cup \{\langle fx, y\rangle \})(fx)=y \) by (rule function_apply_equality )
with y have \( (g \cup \{\langle fx, y\rangle \})(fx)\in N(fx) \)
moreover {
}
ultimately have \( \forall t\in M.\ (g \cup \{\langle fx, y\rangle \})t\in Nt \)
fix \( t \)
assume A: \( t\in M-\{fx\} \)
with g(1) have \( \langle t,gt\rangle \in g \) using apply_Pair
then have \( \langle t,gt\rangle \in (g \cup \{\langle fx, y\rangle \}) \)
then have \( (g \cup \{\langle fx, y\rangle \})t=gt \) using apply_equality, PP
with A have \( (g \cup \{\langle fx, y\rangle \})t\in Nt \) using g(2)
with PP have \( \exists g.\ g\in \text{Pi}(M,\lambda t.\ N t) \wedge (\forall t\in M.\ gt\in Nt) \)
then have \( \forall M N.\ M \preceq succ(x)\wedge (\forall t\in M.\ Nt\neq 0)\longrightarrow (\exists g.\ g \in \text{Pi}(M,\lambda t.\ N t) \wedge (\forall t\in M.\ g t \in N t)) \)
then have \( \text{ the axiom of }succ(x)\text{ choice holds } \) using AxiomCardinalChoiceGen_def, nat_into_Card, as(1), nat_succI
The axiom of choice holds if and only if the AxiomCardinalChoice holds for every couple of a cardinal Q and a set K.
lemma choice_subset_imp_choice:
shows \( \text{ the axiom of } Q \text{ choice holds } \longleftrightarrow (\forall K.\ \text{ the axiom of } Q \text{ choice holds for subsets }K) \) unfolding AxiomCardinalChoice_def, AxiomCardinalChoiceGen_defA choice axiom for greater cardinality implies one for smaller cardinality
lemma greater_choice_imp_smaller_choice:
assumes \( Q\preceq Q1 \), \( \text{Card}(Q) \)
shows \( \text{ the axiom of } Q1 \text{ choice holds } \longrightarrow (\text{ the axiom of } Q \text{ choice holds }) \) using assms, AxiomCardinalChoiceGen_def, lepoll_transIf we have a surjective function from a set which is injective to a set of ordinals, then we can find an injection which goes the other way.
lemma surj_fun_inv:
assumes \( f \in \text{surj}(A,B) \), \( A\subseteq Q \), \( Ord(Q) \)
shows \( B\preceq A \)proof let \( g = \{\langle m,\ \lt mu> j.\ j\in A \wedge f(j)=m\rangle .\ m\in B\} \)
have \( g:B\rightarrow \text{range}(g) \) using lam_is_fun_range
then have fun: \( g:B\rightarrow g(B) \) using range_image_domain
from assms(2,3) have OA: \( \forall j\in A.\ Ord(j) \) using lt_def, Ord_in_Ord
{
fix \( x \)
assume \( x\in g(B) \)
then have \( x\in \text{range}(g) \) and \( \exists y\in B.\ \langle y,x\rangle \in g \)
then obtain \( y \) where T: \( x=(\ \lt mu> j.\ j\in A\wedge f(j)=y) \) and \( y\in B \)
with assms(1), OA obtain \( z \) where P: \( z\in A \wedge f(z)=y \), \( Ord(z) \) unfolding surj_def
with T have \( x\in A \wedge f(x)=y \) using LeastI
hence \( x\in A \)
then have \( g(B) \subseteq A \)
with fun have fun2: \( g:B\rightarrow A \) using fun_weaken_type
then have \( g\in \text{inj}(B,A) \)proof
{
}
fix \( w \) \( x \)
assume AS: \( gw=gx \), \( w\in B \), \( x\in B \)
from assms(1), OA, AS(2,3) obtain \( wz \) \( xz \) where P1: \( wz\in A \wedge f(wz)=w \), \( Ord(wz) \) and P2: \( xz\in A \wedge f(xz)=x \), \( Ord(xz) \) unfolding surj_def
from P1 have \( (\ \lt mu> j.\ j\in A\wedge fj=w) \in A \wedge f(\ \lt mu> j.\ j\in A\wedge fj=w)=w \) by (rule LeastI )
moreover
from P2 have \( (\ \lt mu> j.\ j\in A\wedge fj=x) \in A \wedge f(\ \lt mu> j.\ j\in A\wedge fj=x)=x \) by (rule LeastI )
ultimately have R: \( f(\ \lt mu> j.\ j\in A\wedge fj=w)=w \), \( f(\ \lt mu> j.\ j\in A\wedge fj=x)=x \)
from AS have \( (\ \lt mu> j.\ j\in A\wedge f(j)=w)=(\ \lt mu> j.\ j\in A \wedge f(j)=x) \) using apply_equality, fun2
hence \( f(\ \lt mu> j.\ j\in A \wedge f(j)=w) = f(\ \lt mu> j.\ j\in A \wedge f(j)=x) \)
with R(1) have \( w = f(\ \lt mu> j.\ j\in A\wedge fj=x) \)
with R(2) have \( w=x \)
hence \( \forall w\in B.\ \forall x\in B.\ g(w) = g(x) \longrightarrow w = x \)
with fun2 show \( g\in \text{inj}(B,A) \) unfolding inj_def
qed
then show \( thesis \) unfolding lepoll_def
qed
The difference with the previous result is that in this one A is not a subset of an ordinal, it is only injective with one.
theorem surj_fun_inv_2:
assumes \( f:\text{surj}(A,B) \), \( A\preceq Q \), \( Ord(Q) \)
shows \( B\preceq A \)proof from assms(2) obtain \( h \) where h_def: \( h\in \text{inj}(A,Q) \) using lepoll_def
then have bij: \( h\in \text{bij}(A,\text{range}(h)) \) using inj_bij_range
then obtain \( h1 \) where \( h1\in \text{bij}(\text{range}(h),A) \) using bij_converse_bij
then have \( h1 \in \text{surj}(\text{range}(h),A) \) using bij_def
with assms(1) have \( (f\circ h1)\in \text{surj}(\text{range}(h),B) \) using comp_surj
moreover {
}
fix \( x \)
assume p: \( x\in \text{range}(h) \)
from bij have \( h\in \text{surj}(A,\text{range}(h)) \) using bij_def
with p obtain \( q \) where \( q\in A \) and \( h(q)=x \) using surj_def
then have \( x\in Q \) using h_def, inj_def
then have \( \text{range}(h)\subseteq Q \)
ultimately have \( B\preceq \text{range}(h) \) using surj_fun_inv, assms(3)
moreover
qed
have \( \text{range}(h)\approx A \) using bij, eqpoll_def, eqpoll_sym
ultimately show \( B\preceq A \) using lepoll_eq_trans
end
Definition of LimitC:
\( \text{LimitC}(i) \equiv \text{Card}(i) \wedge 0 \lt i \wedge (\forall y.\ (y \lt i\wedge \text{Card}(y)) \longrightarrow \text{csucc}(y) \lt i) \)
lemma le_imp_lesspoll:
assumes \( \text{Card}(Q) \)
shows \( A \leq Q \Longrightarrow A \preceq Q \) lemma Ord_linear_lt_IML:
assumes \( Ord(i) \), \( Ord(j) \)
shows \( i \lt j \vee i=j \vee j \lt i \) lemma csucc_inf_imp_inf:
assumes \( \text{Card}(j) \) and \( \text{InfCard}(\text{csucc}(j)) \)
shows \( \text{InfCard}(j) \) lemma nat_less_infty:
assumes \( n\in nat \) and \( \text{InfCard}(X) \)
shows \( n \lt X \)Definition of AxiomCardinalChoiceGen:
\( \text{ the axiom of } Q \text{ choice holds } \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)
lemma bij_restrict_rem:
assumes \( f \in \text{bij}(A,B) \) and \( a\in A \)
shows \( \text{restrict}(f, A\setminus \{a\}) \in \text{bij}(A\setminus \{a\}, B\setminus \{f(a)\}) \)Definition of AxiomCardinalChoice:
\( \text{ the axiom of } Q \text{ choice holds for subsets }K \equiv \text{Card}(Q) \wedge (\forall M N.\ (M \preceq Q \wedge (\forall t\in M.\ Nt\neq 0 \wedge Nt\subseteq K)) \longrightarrow (\exists f.\ f:\text{Pi}(M,\lambda t.\ Nt) \wedge (\forall t\in M.\ ft\in Nt))) \)
lemma lam_is_fun_range:
assumes \( f=\{\langle x,g(x)\rangle .\ x\in X\} \)
shows \( f:X\rightarrow \text{range}(f) \) lemma range_image_domain:
assumes \( f:X\rightarrow Y \)
shows \( f(X) = \text{range}(f) \) lemma inj_bij_range:
assumes \( f \in \text{inj}(A,B) \)
shows \( f \in \text{bij}(A,\text{range}(f)) \) lemma surj_fun_inv:
assumes \( f \in \text{surj}(A,B) \), \( A\subseteq Q \), \( Ord(Q) \)
shows \( B\preceq A \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8