theory Order_ZF imports Fol1
begin
This theory file considers various notion related to order. We redefine the notions of a preorder, directed set, total order, linear order and partial order to have the same terminology as Wikipedia (I found it very consistent across different areas of math). We also define and study the notions of intervals and bounded sets. We show the inclusion relations between the intervals with endpoints being in certain order. We also show that union of bounded sets are bounded. This allows to show in Finite_ZF.thy that finite sets are bounded.
Definitions
In this section we formulate the definitions related to order relations.
A relation \(r\) is ''total'' on a set \(X\) if for all elements \(a,b\) of \(X\) we have \(a\) is in relation with \(b\) or \(b\) is in relation with \(a\). An example is the \(\leq \) relation on numbers.
definition
\( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
A relation \(r\) is a partial order on \(X\) if it is reflexive on \(X\) (i.e. \(\langle x,x \rangle\) for every \(x\in X\)), antisymmetric (if \(\langle x, y\rangle \in r \) and \(\langle y, x\rangle \in r \), then \(x=y\)) and transitive \(\langle x, y\rangle \in r \) and \(\langle y, z\rangle \in r \) implies \(\langle x, z\rangle \in r \)).
definition
\( \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) \)
A relation that is reflexive and transitive is called a preorder.
definition
\( \text{IsPreorder}(X,r) \equiv \text{refl}(X,r) \wedge \text{trans}(r) \)
We say that a relation \(r\) up-directs a set if every two-element subset of \(X\) has an upper bound.
definition
\( r \text{ up-directs } X \equiv X\neq 0 \wedge (\forall x\in X.\ \forall y\in X.\ \exists z\in X.\ \langle x,z\rangle \in r \wedge \langle y,z\rangle \in r) \)
Analogously we say that a relation \(r\) down-directs a set if every two-element subset of \(X\) has a lower bound.
definition
\( 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) \)
Typically the notion that is actually defined is the notion of a directed set. or an upward directed set, rather than \(r\) down-directs \(X\) (or \(r\) up-directs \(X\)). This is a nonempty set \(X\) together which a preorder \(r\) such that \(r\) up-directs \(X\). We set that up in separate definitions as we sometimes want to use an upward or downward directed set with a partial order rather than a preorder.
definition
\( \text{IsUpDirectedSet}(X,r) \equiv \text{IsPreorder}(X,r) \wedge (r \text{ up-directs } X) \)
We define the notion of a downward directed set analogously.
definition
\( \text{IsDownDirectedSet}(X,r) \equiv \text{IsPreorder}(X,r) \wedge (r \text{ down-directs } X) \)
We define a linear order as a binary relation that is antisymmetric, transitive and total. Note that this terminology is different than the one used the standard Order.thy file.
definition
\( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
A set is bounded above if there is that is an upper bound for it, i.e. there are some \(u\) such that \(\langle x, u\rangle \in r\) for all \(x\in A\). In addition, the empty set is defined as bounded.
definition
\( \text{IsBoundedAbove}(A,r) \equiv ( A=0 \vee (\exists u.\ \forall x\in A.\ \langle x,u\rangle \in r)) \)
We define sets bounded below analogously.
definition
\( \text{IsBoundedBelow}(A,r) \equiv (A=0 \vee (\exists l.\ \forall x\in A.\ \langle l,x\rangle \in r)) \)
A set is bounded if it is bounded below and above.
definition
\( \text{IsBounded}(A,r) \equiv ( \text{IsBoundedAbove}(A,r) \wedge \text{IsBoundedBelow}(A,r)) \)
The notation for the definition of an interval may be mysterious for some readers, see lemma Order_ZF_2_L1 for more intuitive notation.
definition
\( \text{Interval}(r,a,b) \equiv r\{a\} \cap r^{-1}\{b\} \)
We also define the maximum (the greater of) two elemnts in the obvious way.
definition
\( \text{GreaterOf}(r,a,b) \equiv (\text{if }\langle a,b\rangle \in r\text{ then }b\text{ else }a) \)
The definition a a minimum (the smaller of) two elements.
definition
\( \text{SmallerOf}(r,a,b) \equiv (\text{if }\langle a,b\rangle \in r\text{ then }a\text{ else }b) \)
We say that a set has a maximum if it has an element that is not smaller that any other one. We show that under some conditions this element of the set is unique (if exists).
definition
\( \text{HasAmaximum}(r,A) \equiv \exists M\in A.\ \forall x\in A.\ \langle x,M\rangle \in r \)
A similar definition what it means that a set has a minimum.
definition
\( \text{HasAminimum}(r,A) \equiv \exists m\in A.\ \forall x\in A.\ \langle m,x\rangle \in r \)
Definition of the maximum of a set.
definition
\( \text{Maximum}(r,A) \equiv \text{The } M.\ M\in A \wedge (\forall x\in A.\ \langle x,M\rangle \in r) \)
Definition of a minimum of a set.
definition
\( \text{Minimum}(r,A) \equiv \text{The } m.\ m\in A \wedge (\forall x\in A.\ \langle m,x\rangle \in r) \)
The supremum of a set \(A\) is defined as the minimum of the set of upper bounds, i.e. the set \(\{u.\forall_{a\in A} \langle a,u\rangle \in r\}=\bigcap_{a\in A} r\{a\}\). Recall that in Isabelle/ZF \( r^{-1}(A) \) denotes the inverse image of the set \(A\) by relation \(r\) (i.e. \( r^{-1}(A) \)=\(\{ x: \langle x,y\rangle\in r\) for some \(y\in A\}\)).
definition
\( \text{Supremum}(r,A) \equiv \text{Minimum}(r,\bigcap a\in A.\ r\{a\}) \)
The notion of "having a supremum" is the same as the set of upper bounds having a minimum, but having it a a separate notion does simplify notation in some cases. The definition is written in terms of images of singletons \(\{ x\}\) under relation. To understand this formulation note that the set of upper bounds of a set \(A\subseteq X\) is \(\bigcap_{x\in A}\{ y\in X | \langle x,y\rangle \in r \}\), which is the same as \(\bigcap_{x\in A} r(\{ x \})\), where \(r(\{ x \})\) is the image of the singleton \(\{ x\}\) under relation \(r\).
definition
\( \text{HasAsupremum}(r,A) \equiv \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)
The notion of "having an infimum" is the same as the set of lower bounds having a maximum.
definition
\( \text{HasAnInfimum}(r,A) \equiv \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)
Infimum is defined analogously.
definition
\( \text{Infimum}(r,A) \equiv \text{Maximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)
We define a relation to be complete if every nonempty bounded above set has a supremum.
definition
\( r \text{ is complete } \equiv \) \( \forall A.\ \text{IsBoundedAbove}(A,r) \wedge A\neq 0 \longrightarrow \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)
If a relation down-directs a set, then a larger one does as well.
lemma down_dir_mono:
assumes \( r \text{ down-directs } X \), \( r\subseteq R \)
shows \( R \text{ down-directs } X \) using assms unfolding DownDirects_defIf a relation up-directs a set, then a larger one does as well.
lemma up_dir_mono:
assumes \( r \text{ up-directs } X \), \( r\subseteq R \)
shows \( R \text{ up-directs } X \) using assms unfolding UpDirects_defThe essential condition to show that a total relation is reflexive.
lemma Order_ZF_1_L1:
assumes \( r \text{ is total on } X \) and \( a\in X \)
shows \( \langle a,a\rangle \in r \) using assms, IsTotal_defA total relation is reflexive.
lemma total_is_refl:
assumes \( r \text{ is total on } X \)
shows \( \text{refl}(X,r) \) using assms, Order_ZF_1_L1, refl_defA linear order is partial order.
lemma Order_ZF_1_L2:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( \text{IsPartOrder}(X,r) \) using assms, IsLinOrder_def, IsPartOrder_def, refl_def, Order_ZF_1_L1Partial order that is total is linear.
lemma Order_ZF_1_L3:
assumes \( \text{IsPartOrder}(X,r) \) and \( r \text{ is total on } X \)
shows \( \text{IsLinOrder}(X,r) \) using assms, IsPartOrder_def, IsLinOrder_defRelation that is total on a set is total on any subset.
lemma Order_ZF_1_L4:
assumes \( r \text{ is total on } X \) and \( A\subseteq X \)
shows \( r \text{ is total on } A \) using assms, IsTotal_defWe can restrict a partial order relation to the domain.
lemma part_ord_restr:
assumes \( \text{IsPartOrder}(X,r) \)
shows \( \text{IsPartOrder}(X,r \cap X\times X) \) using assms unfolding IsPartOrder_def, refl_def, antisym_def, trans_defWe can restrict a total order relation to the domain.
lemma total_ord_restr:
assumes \( r \text{ is total on } X \)
shows \( (r \cap X\times X) \text{ is total on } X \) using assms unfolding IsTotal_defA linear relation is linear on any subset and we can restrict it to any subset.
lemma ord_linear_subset:
assumes \( \text{IsLinOrder}(X,r) \) and \( A\subseteq X \)
shows \( \text{IsLinOrder}(A,r) \) and \( \text{IsLinOrder}(A,r \cap A\times A) \)proof from assms show \( \text{IsLinOrder}(A,r) \) using IsLinOrder_def, Order_ZF_1_L4
then have \( \text{IsPartOrder}(A,r \cap A\times A) \) and \( (r \cap A\times A) \text{ is total on } A \) using Order_ZF_1_L2, part_ord_restr, total_ord_restr unfolding IsLinOrder_def
then show \( \text{IsLinOrder}(A,r \cap A\times A) \) using Order_ZF_1_L3
qed
If the relation is total, then every set is a union of those elements that are nongreater than a given one and nonsmaller than a given one.
lemma Order_ZF_1_L5:
assumes \( r \text{ is total on } X \) and \( A\subseteq X \) and \( a\in X \)
shows \( A = \{x\in A.\ \langle x,a\rangle \in r\} \cup \{x\in A.\ \langle a,x\rangle \in r\} \) using assms, IsTotal_defA technical fact about reflexive relations.
lemma refl_add_point:
assumes \( \text{refl}(X,r) \) and \( A \subseteq B \cup \{x\} \) and \( B \subseteq X \) and \( x \in X \) and \( \forall y\in B.\ \langle y,x\rangle \in r \)
shows \( \forall a\in A.\ \langle a,x\rangle \in r \) using assms, refl_defIntervals
In this section we discuss intervals.
The next lemma explains the notation of the definition of an interval.
lemma Order_ZF_2_L1:
shows \( x \in \text{Interval}(r,a,b) \longleftrightarrow \langle a,x\rangle \in r \wedge \langle x,b\rangle \in r \) using Interval_defSince there are some problems with applying the above lemma (seems that simp and auto don't handle equivalence very well), we split Order_ZF_2_L1 into two lemmas.
lemma Order_ZF_2_L1A:
assumes \( x \in \text{Interval}(r,a,b) \)
shows \( \langle a,x\rangle \in r \), \( \langle x,b\rangle \in r \) using assms, Order_ZF_2_L1Order_ZF_2_L1, implication from right to left.
lemma Order_ZF_2_L1B:
assumes \( \langle a,x\rangle \in r \), \( \langle x,b\rangle \in r \)
shows \( x \in \text{Interval}(r,a,b) \) using assms, Order_ZF_2_L1If the relation is reflexive, the endpoints belong to the interval.
lemma Order_ZF_2_L2:
assumes \( \text{refl}(X,r) \) and \( a\in X \), \( b\in X \) and \( \langle a,b\rangle \in r \)
shows \( a \in \text{Interval}(r,a,b) \), \( b \in \text{Interval}(r,a,b) \) using assms, refl_def, Order_ZF_2_L1Under the assumptions of Order_ZF_2_L2, the interval is nonempty.
lemma Order_ZF_2_L2A:
assumes \( \text{refl}(X,r) \) and \( a\in X \), \( b\in X \) and \( \langle a,b\rangle \in r \)
shows \( \text{Interval}(r,a,b) \neq 0 \)proof from assms have \( a \in \text{Interval}(r,a,b) \) using Order_ZF_2_L2
then show \( \text{Interval}(r,a,b) \neq 0 \)
qed
If \(a,b,c,d\) are in this order, then \([b,c]\subseteq [a,d]\). We only need trasitivity for this to be true.
lemma Order_ZF_2_L3:
assumes A1: \( \text{trans}(r) \) and A2: \( \langle a,b\rangle \in r \), \( \langle b,c\rangle \in r \), \( \langle c,d\rangle \in r \)
shows \( \text{Interval}(r,b,c) \subseteq \text{Interval}(r,a,d) \)proof fix \( x \)
assume A3: \( x \in \text{Interval}(r, b, c) \)
note A1
moreover
from A2, A3 have \( \langle a,b\rangle \in r \wedge \langle b,x\rangle \in r \) using Order_ZF_2_L1A
ultimately have T1: \( \langle a,x\rangle \in r \) by (rule Fol1_L3 )
note A1
moreover
qed
from A2, A3 have \( \langle x,c\rangle \in r \wedge \langle c,d\rangle \in r \) using Order_ZF_2_L1A
ultimately have \( \langle x,d\rangle \in r \) by (rule Fol1_L3 )
with T1 show \( x \in \text{Interval}(r,a,d) \) using Order_ZF_2_L1B
For reflexive and antisymmetric relations the interval with equal endpoints consists only of that endpoint.
lemma Order_ZF_2_L4:
assumes A1: \( \text{refl}(X,r) \) and A2: \( \text{antisym}(r) \) and A3: \( a\in X \)
shows \( \text{Interval}(r,a,a) = \{a\} \)proof from A1, A3 have \( \langle a,a\rangle \in r \) using refl_def
with A1, A3 show \( \{a\} \subseteq \text{Interval}(r,a,a) \) using Order_ZF_2_L2
from A2 show \( \text{Interval}(r,a,a) \subseteq \{a\} \) using Order_ZF_2_L1A, Fol1_L4
qed
For transitive relations the endpoints have to be in the relation for the interval to be nonempty.
lemma Order_ZF_2_L5:
assumes A1: \( \text{trans}(r) \) and A2: \( \langle a,b\rangle \notin r \)
shows \( \text{Interval}(r,a,b) = 0 \)proof{
}
assume \( \text{Interval}(r,a,b)\neq 0 \)
then obtain \( x \) where \( x \in \text{Interval}(r,a,b) \)
with A1, A2 have \( False \) using Order_ZF_2_L1A, Fol1_L3
thus \( thesis \)
qed
If a relation is defined on a set, then intervals are subsets of that set.
lemma Order_ZF_2_L6:
assumes A1: \( r \subseteq X\times X \)
shows \( \text{Interval}(r,a,b) \subseteq X \) using assms, Interval_defBounded sets
In this section we consider properties of bounded sets.
For reflexive relations singletons are bounded.
lemma Order_ZF_3_L1:
assumes \( \text{refl}(X,r) \) and \( a\in X \)
shows \( \text{IsBounded}(\{a\},r) \) using assms, refl_def, IsBoundedAbove_def, IsBoundedBelow_def, IsBounded_defSets that are bounded above are contained in the domain of the relation.
lemma Order_ZF_3_L1A:
assumes \( r \subseteq X\times X \) and \( \text{IsBoundedAbove}(A,r) \)
shows \( A\subseteq X \) using assms, IsBoundedAbove_defSets that are bounded below are contained in the domain of the relation.
lemma Order_ZF_3_L1B:
assumes \( r \subseteq X\times X \) and \( \text{IsBoundedBelow}(A,r) \)
shows \( A\subseteq X \) using assms, IsBoundedBelow_defFor a total relation, the greater of two elements, as defined above, is indeed greater of any of the two.
lemma Order_ZF_3_L2:
assumes \( r \text{ is total on } X \) and \( x\in X \), \( y\in X \)
shows \( \langle x, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle y, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),x\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),y\rangle \in r \) using assms, IsTotal_def, Order_ZF_1_L1, GreaterOf_def, SmallerOf_defIf \(A\) is bounded above by \(u\), \(B\) is bounded above by \(w\), then \(A\cup B\) is bounded above by the greater of \(u,w\).
lemma Order_ZF_3_L2B:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( u\in X \), \( w\in X \) and A4: \( \forall x\in A.\ \langle x,u\rangle \in r \), \( \forall x\in B.\ \langle x,w\rangle \in r \)
shows \( \forall x\in A\cup B.\ \langle x, \text{GreaterOf}(r,u,w)\rangle \in r \)proof let \( v = \text{GreaterOf}(r,u,w) \)
from A1, A3 have T1: \( \langle u,v\rangle \in r \) and T2: \( \langle w,v\rangle \in r \) using Order_ZF_3_L2
fix \( x \)
assume A5: \( x\in A\cup B \)
show \( \langle x,v\rangle \in r \)proof
qed
{
}
assume \( x\in A \)
with A4, T1 have \( \langle x,u\rangle \in r \wedge \langle u,v\rangle \in r \)
with A2 have \( \langle x,v\rangle \in r \) by (rule Fol1_L3 )
moreover {
}
ultimately show \( thesis \)
qed
assume \( x\notin A \)
with A5, A4, T2 have \( \langle x,w\rangle \in r \wedge \langle w,v\rangle \in r \)
with A2 have \( \langle x,v\rangle \in r \) by (rule Fol1_L3 )
For total and transitive relation the union of two sets bounded above is bounded above.
lemma Order_ZF_3_L3:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( \text{IsBoundedAbove}(A,r) \), \( \text{IsBoundedAbove}(B,r) \) and A4: \( r \subseteq X\times X \)
shows \( \text{IsBoundedAbove}(A\cup B,r) \)proof{
}
assume \( A=0 \vee B=0 \)
with A3 have \( \text{IsBoundedAbove}(A\cup B,r) \)
moreover {
}
ultimately show \( thesis \)
qed
assume \( \neg (A = 0 \vee B = 0) \)
then have T1: \( A\neq 0 \), \( B\neq 0 \)
with A3 obtain \( u \) \( w \) where D1: \( \forall x\in A.\ \langle x,u\rangle \in r \), \( \forall x\in B.\ \langle x,w\rangle \in r \) using IsBoundedAbove_def
let \( U = \text{GreaterOf}(r,u,w) \)
from T1, A4, D1 have \( u\in X \), \( w\in X \)
with A1, A2, D1 have \( \forall x\in A\cup B.\ \langle x,U\rangle \in r \) using Order_ZF_3_L2B
then have \( \text{IsBoundedAbove}(A\cup B,r) \) using IsBoundedAbove_def
For total and transitive relations if a set \(A\) is bounded above then \(A\cup \{a\}\) is bounded above.
lemma Order_ZF_3_L4:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( \text{IsBoundedAbove}(A,r) \) and A4: \( a\in X \) and A5: \( r \subseteq X\times X \)
shows \( \text{IsBoundedAbove}(A\cup \{a\},r) \)proof from A1 have \( \text{refl}(X,r) \) using total_is_refl
with assms show \( thesis \) using Order_ZF_3_L1, IsBounded_def, Order_ZF_3_L3
qed
If \(A\) is bounded below by \(l\), \(B\) is bounded below by \(m\), then \(A\cup B\) is bounded below by the smaller of \(u,w\).
lemma Order_ZF_3_L5B:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( l\in X \), \( m\in X \) and A4: \( \forall x\in A.\ \langle l,x\rangle \in r \), \( \forall x\in B.\ \langle m,x\rangle \in r \)
shows \( \forall x\in A\cup B.\ \langle \text{SmallerOf}(r,l,m),x\rangle \in r \)proof let \( k = \text{SmallerOf}(r,l,m) \)
from A1, A3 have T1: \( \langle k,l\rangle \in r \) and T2: \( \langle k,m\rangle \in r \) using Order_ZF_3_L2
fix \( x \)
assume A5: \( x\in A\cup B \)
show \( \langle k,x\rangle \in r \)proof
qed
{
}
assume \( x\in A \)
with A4, T1 have \( \langle k,l\rangle \in r \wedge \langle l,x\rangle \in r \)
with A2 have \( \langle k,x\rangle \in r \) by (rule Fol1_L3 )
moreover {
}
ultimately show \( thesis \)
qed
assume \( x\notin A \)
with A5, A4, T2 have \( \langle k,m\rangle \in r \wedge \langle m,x\rangle \in r \)
with A2 have \( \langle k,x\rangle \in r \) by (rule Fol1_L3 )
For total and transitive relation the union of two sets bounded below is bounded below.
lemma Order_ZF_3_L6:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( \text{IsBoundedBelow}(A,r) \), \( \text{IsBoundedBelow}(B,r) \) and A4: \( r \subseteq X\times X \)
shows \( \text{IsBoundedBelow}(A\cup B,r) \)proof{
}
assume \( A=0 \vee B=0 \)
with A3 have \( thesis \)
moreover {
}
ultimately show \( thesis \)
qed
assume \( \neg (A = 0 \vee B = 0) \)
then have T1: \( A\neq 0 \), \( B\neq 0 \)
with A3 obtain \( l \) \( m \) where D1: \( \forall x\in A.\ \langle l,x\rangle \in r \), \( \forall x\in B.\ \langle m,x\rangle \in r \) using IsBoundedBelow_def
let \( L = \text{SmallerOf}(r,l,m) \)
from T1, A4, D1 have T1: \( l\in X \), \( m\in X \)
with A1, A2, D1 have \( \forall x\in A\cup B.\ \langle L,x\rangle \in r \) using Order_ZF_3_L5B
then have \( \text{IsBoundedBelow}(A\cup B,r) \) using IsBoundedBelow_def
For total and transitive relations if a set \(A\) is bounded below then \(A\cup \{a\}\) is bounded below.
lemma Order_ZF_3_L7:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( \text{IsBoundedBelow}(A,r) \) and A4: \( a\in X \) and A5: \( r \subseteq X\times X \)
shows \( \text{IsBoundedBelow}(A\cup \{a\},r) \)proof from A1 have \( \text{refl}(X,r) \) using total_is_refl
with assms show \( thesis \) using Order_ZF_3_L1, IsBounded_def, Order_ZF_3_L6
qed
For total and transitive relations unions of two bounded sets are bounded.
theorem Order_ZF_3_T1:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{IsBounded}(A,r) \), \( \text{IsBounded}(B,r) \) and \( r \subseteq X\times X \)
shows \( \text{IsBounded}(A\cup B,r) \) using assms, Order_ZF_3_L3, Order_ZF_3_L6, Order_ZF_3_L7, IsBounded_defFor total and transitive relations if a set \(A\) is bounded then \(A\cup \{a\}\) is bounded.
lemma Order_ZF_3_L8:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{IsBounded}(A,r) \) and \( a\in X \) and \( r \subseteq X\times X \)
shows \( \text{IsBounded}(A\cup \{a\},r) \) using assms, total_is_refl, Order_ZF_3_L1, Order_ZF_3_T1A sufficient condition for a set to be bounded below.
lemma Order_ZF_3_L9:
assumes A1: \( \forall a\in A.\ \langle l,a\rangle \in r \)
shows \( \text{IsBoundedBelow}(A,r) \)proof from A1 have \( \exists l.\ \forall x\in A.\ \langle l,x\rangle \in r \)
then show \( \text{IsBoundedBelow}(A,r) \) using IsBoundedBelow_def
qed
A sufficient condition for a set to be bounded above.
lemma Order_ZF_3_L10:
assumes A1: \( \forall a\in A.\ \langle a,u\rangle \in r \)
shows \( \text{IsBoundedAbove}(A,r) \)proof from A1 have \( \exists u.\ \forall x\in A.\ \langle x,u\rangle \in r \)
then show \( \text{IsBoundedAbove}(A,r) \) using IsBoundedAbove_def
qed
Intervals are bounded.
lemma Order_ZF_3_L11:
shows \( \text{IsBoundedAbove}( \text{Interval}(r,a,b),r) \), \( \text{IsBoundedBelow}( \text{Interval}(r,a,b),r) \), \( \text{IsBounded}( \text{Interval}(r,a,b),r) \)proof{
}
fix \( x \)
assume \( x \in \text{Interval}(r,a,b) \)
then have \( \langle x,b\rangle \in r \), \( \langle a,x\rangle \in r \) using Order_ZF_2_L1A
then have \( \exists u.\ \forall x\in \text{Interval}(r,a,b).\ \langle x,u\rangle \in r \), \( \exists l.\ \forall x\in \text{Interval}(r,a,b).\ \langle l,x\rangle \in r \)
then show \( \text{IsBoundedAbove}( \text{Interval}(r,a,b),r) \), \( \text{IsBoundedBelow}( \text{Interval}(r,a,b),r) \), \( \text{IsBounded}( \text{Interval}(r,a,b),r) \) using IsBoundedAbove_def, IsBoundedBelow_def, IsBounded_def
qed
A subset of a set that is bounded below is bounded below.
lemma Order_ZF_3_L12:
assumes A1: \( \text{IsBoundedBelow}(A,r) \) and A2: \( B\subseteq A \)
shows \( \text{IsBoundedBelow}(B,r) \)proof{
}
assume \( A = 0 \)
with assms have \( \text{IsBoundedBelow}(B,r) \) using IsBoundedBelow_def
moreover {
}
ultimately show \( \text{IsBoundedBelow}(B,r) \)
qed
assume \( A \neq 0 \)
with A1 have \( \exists l.\ \forall x\in A.\ \langle l,x\rangle \in r \) using IsBoundedBelow_def
with A2 have \( \exists l.\ \forall x\in B.\ \langle l,x\rangle \in r \)
then have \( \text{IsBoundedBelow}(B,r) \) using IsBoundedBelow_def
A subset of a set that is bounded above is bounded above.
lemma Order_ZF_3_L13:
assumes A1: \( \text{IsBoundedAbove}(A,r) \) and A2: \( B\subseteq A \)
shows \( \text{IsBoundedAbove}(B,r) \)proof{
}
assume \( A = 0 \)
with assms have \( \text{IsBoundedAbove}(B,r) \) using IsBoundedAbove_def
moreover {
}
ultimately show \( \text{IsBoundedAbove}(B,r) \)
qed
assume \( A \neq 0 \)
with A1 have \( \exists u.\ \forall x\in A.\ \langle x,u\rangle \in r \) using IsBoundedAbove_def
with A2 have \( \exists u.\ \forall x\in B.\ \langle x,u\rangle \in r \)
then have \( \text{IsBoundedAbove}(B,r) \) using IsBoundedAbove_def
If for every element of \(X\) we can find one in \(A\) that is greater, then the \(A\) can not be bounded above. Works for relations that are total, transitive and antisymmetric, (i.e. for linear order relations).
lemma Order_ZF_3_L14:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( \text{antisym}(r) \) and A4: \( r \subseteq X\times X \) and A5: \( X\neq 0 \) and A6: \( \forall x\in X.\ \exists a\in A.\ x\neq a \wedge \langle x,a\rangle \in r \)
shows \( \neg \text{IsBoundedAbove}(A,r) \)proof{
}
from A5, A6 have I: \( A\neq 0 \)
moreover
assume \( \text{IsBoundedAbove}(A,r) \)
ultimately obtain \( u \) where II: \( \forall x\in A.\ \langle x,u\rangle \in r \) using IsBounded_def, IsBoundedAbove_def
with A4, I have \( u\in X \)
with A6 obtain \( b \) where \( b\in A \) and III: \( u\neq b \) and \( \langle u,b\rangle \in r \)
with II have \( \langle b,u\rangle \in r \), \( \langle u,b\rangle \in r \)
with A3 have \( b=u \) by (rule Fol1_L4 )
with III have \( False \)
thus \( \neg \text{IsBoundedAbove}(A,r) \)
qed
The set of elements in a set \(A\) that are nongreater than a given element is bounded above.
lemma Order_ZF_3_L15:
shows \( \text{IsBoundedAbove}(\{x\in A.\ \langle x,a\rangle \in r\},r) \) using IsBoundedAbove_defIf \(A\) is bounded below, then the set of elements in a set \(A\) that are nongreater than a given element is bounded.
lemma Order_ZF_3_L16:
assumes A1: \( \text{IsBoundedBelow}(A,r) \)
shows \( \text{IsBounded}(\{x\in A.\ \langle x,a\rangle \in r\},r) \)proof{
}
assume \( A=0 \)
then have \( \text{IsBounded}(\{x\in A.\ \langle x,a\rangle \in r\},r) \) using IsBoundedBelow_def, IsBoundedAbove_def, IsBounded_def
moreover {
}
ultimately show \( thesis \)
qed
assume \( A\neq 0 \)
with A1 obtain \( l \) where I: \( \forall x\in A.\ \langle l,x\rangle \in r \) using IsBoundedBelow_def
then have \( \forall y\in \{x\in A.\ \langle x,a\rangle \in r\}.\ \langle l,y\rangle \in r \)
then have \( \text{IsBoundedBelow}(\{x\in A.\ \langle x,a\rangle \in r\},r) \) by (rule Order_ZF_3_L9 )
then have \( \text{IsBounded}(\{x\in A.\ \langle x,a\rangle \in r\},r) \) using Order_ZF_3_L15, IsBounded_def
end
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 UpDirects:
\( r \text{ up-directs } X \equiv X\neq 0 \wedge (\forall x\in X.\ \forall y\in X.\ \exists z\in X.\ \langle x,z\rangle \in r \wedge \langle y,z\rangle \in r) \)
Definition of IsTotal:
\( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
lemma Order_ZF_1_L1:
assumes \( r \text{ is total on } X \) and \( a\in X \)
shows \( \langle a,a\rangle \in r \)Definition of IsLinOrder:
\( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
Definition of IsPartOrder:
\( \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) \)
lemma Order_ZF_1_L4:
assumes \( r \text{ is total on } X \) and \( A\subseteq X \)
shows \( r \text{ is total on } A \) lemma Order_ZF_1_L2:
assumes \( \text{IsLinOrder}(X,r) \)
shows \( \text{IsPartOrder}(X,r) \) lemma part_ord_restr:
assumes \( \text{IsPartOrder}(X,r) \)
shows \( \text{IsPartOrder}(X,r \cap X\times X) \) lemma total_ord_restr:
assumes \( r \text{ is total on } X \)
shows \( (r \cap X\times X) \text{ is total on } X \) lemma Order_ZF_1_L3:
assumes \( \text{IsPartOrder}(X,r) \) and \( r \text{ is total on } X \)
shows \( \text{IsLinOrder}(X,r) \)Definition of Interval:
\( \text{Interval}(r,a,b) \equiv r\{a\} \cap r^{-1}\{b\} \)
lemma Order_ZF_2_L1: shows \( x \in \text{Interval}(r,a,b) \longleftrightarrow \langle a,x\rangle \in r \wedge \langle x,b\rangle \in r \)
lemma Order_ZF_2_L2:
assumes \( \text{refl}(X,r) \) and \( a\in X \), \( b\in X \) and \( \langle a,b\rangle \in r \)
shows \( a \in \text{Interval}(r,a,b) \), \( b \in \text{Interval}(r,a,b) \) lemma Order_ZF_2_L1A:
assumes \( x \in \text{Interval}(r,a,b) \)
shows \( \langle a,x\rangle \in r \), \( \langle x,b\rangle \in r \) lemma Fol1_L3:
assumes \( \text{trans}(r) \) and \( \langle a,b\rangle \in r \wedge \langle b,c\rangle \in r \)
shows \( \langle a,c\rangle \in r \) lemma Order_ZF_2_L1B:
assumes \( \langle a,x\rangle \in r \), \( \langle x,b\rangle \in r \)
shows \( x \in \text{Interval}(r,a,b) \) lemma Fol1_L4:
assumes \( \text{antisym}(r) \) and \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \)
shows \( a=b \)Definition of IsBoundedAbove:
\( \text{IsBoundedAbove}(A,r) \equiv ( A=0 \vee (\exists u.\ \forall x\in A.\ \langle x,u\rangle \in r)) \)
Definition of IsBoundedBelow:
\( \text{IsBoundedBelow}(A,r) \equiv (A=0 \vee (\exists l.\ \forall x\in A.\ \langle l,x\rangle \in r)) \)
Definition of IsBounded:
\( \text{IsBounded}(A,r) \equiv ( \text{IsBoundedAbove}(A,r) \wedge \text{IsBoundedBelow}(A,r)) \)
Definition of GreaterOf:
\( \text{GreaterOf}(r,a,b) \equiv (\text{if }\langle a,b\rangle \in r\text{ then }b\text{ else }a) \)
Definition of SmallerOf:
\( \text{SmallerOf}(r,a,b) \equiv (\text{if }\langle a,b\rangle \in r\text{ then }a\text{ else }b) \)
lemma Order_ZF_3_L2:
assumes \( r \text{ is total on } X \) and \( x\in X \), \( y\in X \)
shows \( \langle x, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle y, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),x\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),y\rangle \in r \) lemma Order_ZF_3_L2B:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( u\in X \), \( w\in X \) and \( \forall x\in A.\ \langle x,u\rangle \in r \), \( \forall x\in B.\ \langle x,w\rangle \in r \)
shows \( \forall x\in A\cup B.\ \langle x, \text{GreaterOf}(r,u,w)\rangle \in r \) lemma total_is_refl:
assumes \( r \text{ is total on } X \)
shows \( \text{refl}(X,r) \) lemma Order_ZF_3_L1:
assumes \( \text{refl}(X,r) \) and \( a\in X \)
shows \( \text{IsBounded}(\{a\},r) \) lemma Order_ZF_3_L3:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{IsBoundedAbove}(A,r) \), \( \text{IsBoundedAbove}(B,r) \) and \( r \subseteq X\times X \)
shows \( \text{IsBoundedAbove}(A\cup B,r) \) lemma Order_ZF_3_L5B:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( l\in X \), \( m\in X \) and \( \forall x\in A.\ \langle l,x\rangle \in r \), \( \forall x\in B.\ \langle m,x\rangle \in r \)
shows \( \forall x\in A\cup B.\ \langle \text{SmallerOf}(r,l,m),x\rangle \in r \) lemma Order_ZF_3_L6:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{IsBoundedBelow}(A,r) \), \( \text{IsBoundedBelow}(B,r) \) and \( r \subseteq X\times X \)
shows \( \text{IsBoundedBelow}(A\cup B,r) \) lemma Order_ZF_3_L7:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{IsBoundedBelow}(A,r) \) and \( a\in X \) and \( r \subseteq X\times X \)
shows \( \text{IsBoundedBelow}(A\cup \{a\},r) \) theorem Order_ZF_3_T1:
assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{IsBounded}(A,r) \), \( \text{IsBounded}(B,r) \) and \( r \subseteq X\times X \)
shows \( \text{IsBounded}(A\cup B,r) \) lemma Order_ZF_3_L9:
assumes \( \forall a\in A.\ \langle l,a\rangle \in r \)
shows \( \text{IsBoundedBelow}(A,r) \) lemma Order_ZF_3_L15: shows \( \text{IsBoundedAbove}(\{x\in A.\ \langle x,a\rangle \in r\},r) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8