IsarMathLib

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

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_def

If 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_def

The 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_def

A 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_def

A 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_L1

Partial 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_def

Relation 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_def

We 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_def

We 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_def

A 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_def

A 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_def

Intervals

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_def

Since 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_L1

Order_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_L1

If 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_L1

Under 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
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
qed

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_def

Bounded 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_def

Sets 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_def

Sets 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_def

For 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_def

If \(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
{
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 {
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 )
} ultimately show \( thesis \)
qed
qed

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 {
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
} ultimately show \( thesis \)
qed

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
{
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 {
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 )
} ultimately show \( thesis \)
qed
qed

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 {
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
} ultimately show \( thesis \)
qed

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_def

For 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_T1

A 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 {
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
} ultimately show \( \text{IsBoundedBelow}(B,r) \)
qed

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 {
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
} ultimately show \( \text{IsBoundedAbove}(B,r) \)
qed

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_def

If \(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 {
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
} ultimately show \( thesis \)
qed
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) \)