Skip to content

Commit

Permalink
another form of finite choice
Browse files Browse the repository at this point in the history
  • Loading branch information
@SKolodynski
SKolodynski committed Feb 16, 2025
1 parent 24c641d commit ba1a7cc
Show file tree
Hide file tree
Showing 3 changed files with 127 additions and 90 deletions.
210 changes: 121 additions & 89 deletions IsarMathLib/Cardinal_ZF.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)

section \<open>Cardinal numbers\<close>

theory Cardinal_ZF imports ZF.CardinalArith func1
theory Cardinal_ZF imports ZF.CardinalArith Finite_ZF func1

begin

Expand Down Expand Up @@ -408,6 +408,105 @@ definition
AxiomCardinalChoiceGen ("{the axiom of}_{choice holds}") where
"{the axiom of} Q {choice holds} \<equiv> Card(Q) \<and> (\<forall> M N. (M \<lesssim>Q \<and> (\<forall>t\<in>M. N`t\<noteq>0)) \<longrightarrow> (\<exists>f. f:Pi(M,\<lambda>t. N`t) \<and> (\<forall>t\<in>M. f`t\<in>N`t)))"


text\<open>The axiom of choice holds if and only if the \<open>AxiomCardinalChoice\<close>
holds for every couple of a cardinal \<open>Q\<close> and a set \<open>K\<close>.\<close>

lemma choice_subset_imp_choice:
shows "{the axiom of} Q {choice holds} \<longleftrightarrow> (\<forall> K. {the axiom of} Q {choice holds for subsets}K)"
unfolding AxiomCardinalChoice_def AxiomCardinalChoiceGen_def by blast

text\<open>A choice axiom for greater cardinality implies one for
smaller cardinality\<close>

lemma greater_choice_imp_smaller_choice:
assumes "Q\<lesssim>Q1" "Card(Q)"
shows "{the axiom of} Q1 {choice holds} \<longrightarrow> ({the axiom of} Q {choice holds})" using assms
AxiomCardinalChoiceGen_def lepoll_trans by auto

text\<open>If 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.\<close>

lemma surj_fun_inv:
assumes "f \<in> surj(A,B)" "A\<subseteq>Q" "Ord(Q)"
shows "B\<lesssim>A"
proof-
let ?g = "{\<langle>m,\<mu> j. j\<in>A \<and> f`(j)=m\<rangle>. m\<in>B}"
have "?g:B\<rightarrow>range(?g)" using lam_is_fun_range by simp
then have fun: "?g:B\<rightarrow>?g``(B)" using range_image_domain by simp
from assms(2,3) have OA: "\<forall>j\<in>A. Ord(j)" using lt_def Ord_in_Ord by auto
{
fix x
assume "x\<in>?g``(B)"
then have "x\<in>range(?g)" and "\<exists>y\<in>B. \<langle>y,x\<rangle>\<in>?g" by auto
then obtain y where T: "x=(\<mu> j. j\<in>A\<and> f`(j)=y)" and "y\<in>B" by auto
with assms(1) OA obtain z where P: "z\<in>A \<and> f`(z)=y" "Ord(z)" unfolding surj_def
by auto
with T have "x\<in>A \<and> f`(x)=y" using LeastI by simp
hence "x\<in>A" by simp
}
then have "?g``(B) \<subseteq> A" by auto
with fun have fun2: "?g:B\<rightarrow>A" using fun_weaken_type by auto
then have "?g\<in>inj(B,A)"
proof -
{
fix w x
assume AS: "?g`w=?g`x" "w\<in>B" "x\<in>B"
from assms(1) OA AS(2,3) obtain wz xz where
P1: "wz\<in>A \<and> f`(wz)=w" "Ord(wz)" and P2: "xz\<in>A \<and> f`(xz)=x" "Ord(xz)"
unfolding surj_def by blast
from P1 have "(\<mu> j. j\<in>A\<and> f`j=w) \<in> A \<and> f`(\<mu> j. j\<in>A\<and> f`j=w)=w"
by (rule LeastI)
moreover from P2 have "(\<mu> j. j\<in>A\<and> f`j=x) \<in> A \<and> f`(\<mu> j. j\<in>A\<and> f`j=x)=x"
by (rule LeastI)
ultimately have R: "f`(\<mu> j. j\<in>A\<and> f`j=w)=w" "f`(\<mu> j. j\<in>A\<and> f`j=x)=x"
by auto
from AS have "(\<mu> j. j\<in>A\<and> f`(j)=w)=(\<mu> j. j\<in>A \<and> f`(j)=x)"
using apply_equality fun2 by auto
hence "f`(\<mu> j. j\<in>A \<and> f`(j)=w) = f`(\<mu> j. j\<in>A \<and> f`(j)=x)" by auto
with R(1) have "w = f`(\<mu> j. j\<in>A\<and> f`j=x)" by auto
with R(2) have "w=x" by auto
}
hence "\<forall>w\<in>B. \<forall>x\<in>B. ?g`(w) = ?g`(x) \<longrightarrow> w = x"
by auto
with fun2 show "?g\<in>inj(B,A)" unfolding inj_def by auto
qed
then show ?thesis unfolding lepoll_def by auto
qed

text\<open>The difference with the previous result is that in this one
\<open>A\<close> is not a subset of an ordinal, it is only injective
with one.\<close>

theorem surj_fun_inv_2:
assumes "f:surj(A,B)" "A\<lesssim>Q" "Ord(Q)"
shows "B\<lesssim>A"
proof-
from assms(2) obtain h where h_def: "h\<in>inj(A,Q)" using lepoll_def by auto
then have bij: "h\<in>bij(A,range(h))" using inj_bij_range by auto
then obtain h1 where "h1\<in>bij(range(h),A)" using bij_converse_bij by auto
then have "h1 \<in> surj(range(h),A)" using bij_def by auto
with assms(1) have "(f O h1)\<in>surj(range(h),B)" using comp_surj by auto
moreover
{
fix x
assume p: "x\<in>range(h)"
from bij have "h\<in>surj(A,range(h))" using bij_def by auto
with p obtain q where "q\<in>A" and "h`(q)=x" using surj_def by auto
then have "x\<in>Q" using h_def inj_def by auto
}
then have "range(h)\<subseteq>Q" by auto
ultimately have "B\<lesssim>range(h)" using surj_fun_inv assms(3) by auto
moreover have "range(h)\<approx>A" using bij eqpoll_def eqpoll_sym by blast
ultimately show "B\<lesssim>A" using lepoll_eq_trans by auto
qed

subsection\<open>Finite choice\<close>

text\<open>In ZF every finite collection of non-empty sets has a choice function, i.e. a function that
selects one element from each set of the collection. In this section we prove various forms of
that claim.\<close>

text\<open>The axiom of finite choice always holds.\<close>

theorem finite_choice:
Expand Down Expand Up @@ -497,97 +596,30 @@ proof -
ultimately show ?thesis by (rule nat_induct)
qed

text\<open>The axiom of choice holds if and only if the \<open>AxiomCardinalChoice\<close>
holds for every couple of a cardinal \<open>Q\<close> and a set \<open>K\<close>.\<close>

lemma choice_subset_imp_choice:
shows "{the axiom of} Q {choice holds} \<longleftrightarrow> (\<forall> K. {the axiom of} Q {choice holds for subsets}K)"
unfolding AxiomCardinalChoice_def AxiomCardinalChoiceGen_def by blast

text\<open>A choice axiom for greater cardinality implies one for
smaller cardinality\<close>
text\<open>The choice functions of a collection $\mathcal{A}$ are functions $f$ defined on
$\mathcal{A}$ and valued in $\bigcup \mathcal{A}$ such that $f(A)\in A$
for every $A\in \mathcal{A}$.\<close>

lemma greater_choice_imp_smaller_choice:
assumes "Q\<lesssim>Q1" "Card(Q)"
shows "{the axiom of} Q1 {choice holds} \<longrightarrow> ({the axiom of} Q {choice holds})" using assms
AxiomCardinalChoiceGen_def lepoll_trans by auto

text\<open>If 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.\<close>

lemma surj_fun_inv:
assumes "f \<in> surj(A,B)" "A\<subseteq>Q" "Ord(Q)"
shows "B\<lesssim>A"
proof-
let ?g = "{\<langle>m,\<mu> j. j\<in>A \<and> f`(j)=m\<rangle>. m\<in>B}"
have "?g:B\<rightarrow>range(?g)" using lam_is_fun_range by simp
then have fun: "?g:B\<rightarrow>?g``(B)" using range_image_domain by simp
from assms(2,3) have OA: "\<forall>j\<in>A. Ord(j)" using lt_def Ord_in_Ord by auto
{
fix x
assume "x\<in>?g``(B)"
then have "x\<in>range(?g)" and "\<exists>y\<in>B. \<langle>y,x\<rangle>\<in>?g" by auto
then obtain y where T: "x=(\<mu> j. j\<in>A\<and> f`(j)=y)" and "y\<in>B" by auto
with assms(1) OA obtain z where P: "z\<in>A \<and> f`(z)=y" "Ord(z)" unfolding surj_def
by auto
with T have "x\<in>A \<and> f`(x)=y" using LeastI by simp
hence "x\<in>A" by simp
}
then have "?g``(B) \<subseteq> A" by auto
with fun have fun2: "?g:B\<rightarrow>A" using fun_weaken_type by auto
then have "?g\<in>inj(B,A)"
proof -
{
fix w x
assume AS: "?g`w=?g`x" "w\<in>B" "x\<in>B"
from assms(1) OA AS(2,3) obtain wz xz where
P1: "wz\<in>A \<and> f`(wz)=w" "Ord(wz)" and P2: "xz\<in>A \<and> f`(xz)=x" "Ord(xz)"
unfolding surj_def by blast
from P1 have "(\<mu> j. j\<in>A\<and> f`j=w) \<in> A \<and> f`(\<mu> j. j\<in>A\<and> f`j=w)=w"
by (rule LeastI)
moreover from P2 have "(\<mu> j. j\<in>A\<and> f`j=x) \<in> A \<and> f`(\<mu> j. j\<in>A\<and> f`j=x)=x"
by (rule LeastI)
ultimately have R: "f`(\<mu> j. j\<in>A\<and> f`j=w)=w" "f`(\<mu> j. j\<in>A\<and> f`j=x)=x"
by auto
from AS have "(\<mu> j. j\<in>A\<and> f`(j)=w)=(\<mu> j. j\<in>A \<and> f`(j)=x)"
using apply_equality fun2 by auto
hence "f`(\<mu> j. j\<in>A \<and> f`(j)=w) = f`(\<mu> j. j\<in>A \<and> f`(j)=x)" by auto
with R(1) have "w = f`(\<mu> j. j\<in>A\<and> f`j=x)" by auto
with R(2) have "w=x" by auto
}
hence "\<forall>w\<in>B. \<forall>x\<in>B. ?g`(w) = ?g`(x) \<longrightarrow> w = x"
by auto
with fun2 show "?g\<in>inj(B,A)" unfolding inj_def by auto
qed
then show ?thesis unfolding lepoll_def by auto
qed
definition
"ChoiceFunctions(\<A>) \<equiv> {f\<in>\<A>\<rightarrow>\<Union>\<A>. \<forall>A\<in>\<A>. f`(A)\<in>A}"

text\<open>The difference with the previous result is that in this one
\<open>A\<close> is not a subset of an ordinal, it is only injective
with one.\<close>
text\<open>For finite collections of non-empty sets the set of choice functions is non-empty.\<close>

theorem surj_fun_inv_2:
assumes "f:surj(A,B)" "A\<lesssim>Q" "Ord(Q)"
shows "B\<lesssim>A"
proof-
from assms(2) obtain h where h_def: "h\<in>inj(A,Q)" using lepoll_def by auto
then have bij: "h\<in>bij(A,range(h))" using inj_bij_range by auto
then obtain h1 where "h1\<in>bij(range(h),A)" using bij_converse_bij by auto
then have "h1 \<in> surj(range(h),A)" using bij_def by auto
with assms(1) have "(f O h1)\<in>surj(range(h),B)" using comp_surj by auto
moreover
{
fix x
assume p: "x\<in>range(h)"
from bij have "h\<in>surj(A,range(h))" using bij_def by auto
with p obtain q where "q\<in>A" and "h`(q)=x" using surj_def by auto
then have "x\<in>Q" using h_def inj_def by auto
}
then have "range(h)\<subseteq>Q" by auto
ultimately have "B\<lesssim>range(h)" using surj_fun_inv assms(3) by auto
moreover have "range(h)\<approx>A" using bij eqpoll_def eqpoll_sym by blast
ultimately show "B\<lesssim>A" using lepoll_eq_trans by auto
theorem finite_choice1: assumes "Finite(\<A>)" and "\<forall>A\<in>\<A>. A\<noteq>\<emptyset>"
shows "ChoiceFunctions(\<A>) \<noteq> \<emptyset>"
proof -
let ?N = "id(\<A>)"
let ?\<N> = "(\<lambda>t. ?N`(t))"
from assms(1) obtain n where "n\<in>nat" and "\<A>\<approx>n"
unfolding Finite_def by auto
from assms(2) \<open>\<A>\<approx>n\<close> have "\<A>\<lesssim>n" and "\<forall>A\<in>\<A>. ?N`(A)\<noteq>\<emptyset>"
using eqpoll_imp_lepoll by simp_all
with \<open>n\<in>nat\<close> obtain f where "f\<in>Pi(\<A>,?\<N>)"
using finite_choice unfolding AxiomCardinalChoiceGen_def by blast
have "Pi(\<A>,?\<N>) = {f\<in>\<A>\<rightarrow>(\<Union>A\<in>\<A>. ?\<N>(A)). \<forall>A\<in>\<A>. f`(A)\<in>?\<N>(A)}"
by (rule pi_fun_space)
with \<open>f\<in>Pi(\<A>,?\<N>)\<close> show ?thesis
unfolding ChoiceFunctions_def by auto
qed


end
5 changes: 5 additions & 0 deletions IsarMathLib/Finite_ZF.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,11 @@ lemma card_fin_is_nat: assumes "A \<in> FinPow(X)"
using assms FinPow_def Finite_def cardinal_cong nat_into_Card
Card_cardinal_eq by auto

text\<open>The cardinality of a finite set is a natural number.\<close>

lemma card_fin_is_nat1: assumes "Finite(A)" shows "|A| \<in> nat"
using assms card_fin_is_nat(1) unfolding FinPow_def by auto

text\<open>A reformulation of \<open>card_fin_is_nat\<close>: for a finit
set $A$ there is a bijection between $|A|$ and $A$.\<close>

Expand Down
2 changes: 1 addition & 1 deletion IsarMathLib/func1.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -955,7 +955,7 @@ qed
subsection\<open>Dependent function space\<close>

text\<open>The standard Isabelle/ZF \<open>ZF_Base\<close> theory defines a general notion of
a dependent function space $\text{Pi}(X,N)$, where $X$ wher $X$ is any set and
a dependent function space \<open>Pi(X,N)\<close>, where $X$ is any set and
$N$ is a collection of sets indexed by $X$. We rarely use that notion in IsarMathLib.
The facts shown in this section provide information on how to interpret the
dependent function space notion in terms of a regular space of functions defined on $X$
Expand Down

0 comments on commit ba1a7cc

Please sign in to comment.