IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory FinOrd_ZF_1 imports FinOrd_ZF Cardinal_ZF

begin

In this theory we continue the subject of finite sets and order relation from FinOrd_ZF with some consequences of finite choice for down-directed sets.

Finte choice and preorders

In the Order_ZF theory we define what it means that a relation \(r\) down-directs a set \(X\): each two elements of \(X\) have a common lower bound in \(X\). If the relation is a preorder (i.e. is reflexive and transitive) and it down-directs \(X\) we say that \(X\) is a down-directed set (by the relation \(r\)).

The next lemma states that each finite subset of a down-directed set has a lower bound in \(X\).

lemma fin_dir_set_bounded:

assumes \( \text{IsDownDirectedSet}(X,r) \) and \( B\in \text{FinPow}(X) \)

shows \( \exists x\in X.\ \forall t\in B.\ \langle x,t\rangle \in r \)proof

from assms(1) have \( \exists x\in X.\ \forall t\in \emptyset .\ \langle x,t\rangle \in r \) unfolding IsDownDirectedSet_def, DownDirects_def

moreover

have \( \forall A\in \text{FinPow}(X).\ (\exists x\in X.\ \forall t\in A.\ \langle x,t\rangle \in r)\longrightarrow (\forall a\in X.\ \exists m\in X.\ \forall t\in A\cup \{a\}.\ \langle m,t\rangle \in r) \)proof

{

fix \( A \)

assume \( A\in \text{FinPow}(X) \) and I: \( \exists x\in X.\ \forall t\in A.\ \langle x,t\rangle \in r \)

{

fix \( a \)

assume \( a\in X \)

from I obtain \( x \) where \( x\in X \) and II: \( \forall t\in A.\ \langle x,t\rangle \in r \)

from assms(1), \( a\in X \), \( x\in X \) obtain \( m \) where \( m\in X \), \( \langle m,a\rangle \in r \), \( \langle m,x\rangle \in r \) unfolding IsDownDirectedSet_def, DownDirects_def

with assms(1), II have \( \exists m\in X.\ \forall t\in A\cup \{a\}.\ \langle m,t\rangle \in r \) unfolding IsDownDirectedSet_def, IsPreorder_def, trans_def

}

hence \( \forall a\in X.\ \exists x\in X.\ \forall t\in A\cup \{a\}.\ \langle x,t\rangle \in r \)

}

thus \( thesis \)

qed

moreover

note assms(2)

ultimately show \( thesis \) by (rule FinPow_induct )

qed

Suppose \(Y\) is a set down-directed by a (preorder) relation \(r\) and \(f,g\) are funtions defined on two finite subsets \(A,B\), resp., of \(X\), valued in Y (i.e.\(f:A\rightarrow Y\), \(f:B\rightarrow Y\) and \(A,B\) are finite subsets of \(X\)). Then there exist a function \(h:A\cup B\rightarrow Y\) that is a lower bound for \(f\) on \(A\) and for \(g\) on \(B\).

lemma two_fun_low_bound:

assumes \( \text{IsDownDirectedSet}(Y,r) \), \( A\in \text{FinPow}(X) \), \( B\in \text{FinPow}(X) \), \( f:A\rightarrow Y \), \( g:B\rightarrow Y \)

shows \( \exists h\in A\cup B\rightarrow Y.\ (\forall x\in A.\ \langle h(x),f(x)\rangle \in r) \wedge (\forall x\in B.\ \langle h(x),g(x)\rangle \in r) \)proof

from assms(2,3) have \( Finite(A\cup B) \) using union_finpow unfolding FinPow_def

{

fix \( x \)

assume \( x\in A\cup B \)

from assms(4,5) have \( f\{x\}\cup g\{x\} \in \text{FinPow}(Y) \) using image_singleton_fin, union_finpow

with assms(1) have \( \exists y\in Y.\ \forall t\in (f\{x\}\cup g\{x\}).\ \langle y,t\rangle \in r \) using fin_dir_set_bounded

}

hence \( \forall x\in A\cup B.\ \exists y\in Y.\ \forall t\in (f\{x\}\cup g\{x\}).\ \langle y,t\rangle \in r \)

with \( Finite(A\cup B) \) have \( \exists h\in A\cup B\rightarrow Y.\ \forall x\in A\cup B.\ \forall t\in (f\{x\}\cup g\{x\}).\ \langle h(x),t\rangle \in r \) by (rule finite_choice_fun )

then obtain \( h \) where \( h\in A\cup B\rightarrow Y \) and \( \forall x\in A\cup B.\ \forall t\in (f\{x\}\cup g\{x\}).\ \langle h(x),t\rangle \in r \)

with assms(4,5) have \( \forall x\in A.\ \langle h(x),f(x)\rangle \in r \) and \( \forall x\in B.\ \langle h(x),g(x)\rangle \in r \) using func_imagedef

with \( h\in A\cup B\rightarrow Y \) show \( thesis \)

qed

end

Definition of IsDownDirectedSet: \( \text{IsDownDirectedSet}(X,r) \equiv \text{IsPreorder}(X,r) \wedge (r \text{ down-directs } X) \)

Definition of DownDirects: \( r \text{ down-directs } X \equiv X\neq 0 \wedge (\forall x\in X.\ \forall y\in X.\ \exists z\in X.\ \langle z,x\rangle \in r \wedge \langle z,y\rangle \in r) \)

Definition of IsPreorder: \( \text{IsPreorder}(X,r) \equiv \text{refl}(X,r) \wedge \text{trans}(r) \)

theorem FinPow_induct:

assumes \( P(0) \) and \( \forall A \in \text{FinPow}(X).\ P(A) \longrightarrow (\forall a\in X.\ P(A \cup \{a\})) \) and \( B \in \text{FinPow}(X) \)

shows \( P(B) \)

lemma union_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \in \text{FinPow}(X) \)

shows \( A \cup B \in \text{FinPow}(X) \)

Definition of FinPow: \( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)

lemma image_singleton_fin:

assumes \( f:X\rightarrow Y \)

shows \( f\{x\} \in \text{FinPow}(Y) \)

lemma fin_dir_set_bounded:

assumes \( \text{IsDownDirectedSet}(X,r) \) and \( B\in \text{FinPow}(X) \)

shows \( \exists x\in X.\ \forall t\in B.\ \langle x,t\rangle \in r \)

lemma finite_choice_fun: