theory Order_ZF_1a imports Order_ZF
begin
This theory is a continuation of Order_ZF and talks about maximuma and minimum of a set, supremum and infimum and strict (not reflexive) versions of order relations.
Maximum and minimum of a set
In this section we show that maximum and minimum are unique if they exist. We also show that union of sets that have maxima (minima) has a maximum (minimum). We also show that singletons have maximum and minimum. All this allows to show (in Finite_ZF) that every finite set has well-defined maximum and minimum.
A somewhat technical fact that allows to reduce the number of premises in some theorems: the assumption that a set has a maximum implies that it is not empty.
lemma set_max_not_empty:
assumes \( \text{HasAmaximum}(r,A) \)
shows \( A\neq 0 \) using assms unfolding HasAmaximum_defIf a set has a maximum implies that it is not empty.
lemma set_min_not_empty:
assumes \( \text{HasAminimum}(r,A) \)
shows \( A\neq 0 \) using assms unfolding HasAminimum_defIf a set has a supremum then it cannot be empty. We are probably using the fact that \(\bigcap \emptyset = \emptyset \), which makes me a bit anxious as this I think is just a convention.
lemma set_sup_not_empty:
assumes \( \text{HasAsupremum}(r,A) \)
shows \( A\neq 0 \)proof from assms have \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \) unfolding HasAsupremum_def
then have \( (\bigcap a\in A.\ r\{a\}) \neq 0 \) using set_min_not_empty
then obtain \( x \) where \( x \in (\bigcap y\in A.\ r\{y\}) \)
thus \( thesis \)
qed
If a set has an infimum then it cannot be empty.
lemma set_inf_not_empty:
assumes \( \text{HasAnInfimum}(r,A) \)
shows \( A\neq 0 \)proof from assms have \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \) unfolding HasAnInfimum_def
then have \( (\bigcap a\in A.\ r^{-1}\{a\}) \neq 0 \) using set_max_not_empty
then obtain \( x \) where \( x \in (\bigcap y\in A.\ r^{-1}\{y\}) \)
thus \( thesis \)
qed
For antisymmetric relations maximum of a set is unique if it exists.
lemma Order_ZF_4_L1:
assumes A1: \( \text{antisym}(r) \) and A2: \( \text{HasAmaximum}(r,A) \)
shows \( \exists !M.\ M\in A \wedge (\forall x\in A.\ \langle x,M\rangle \in r) \)proof from A2 show \( \exists M.\ M \in A \wedge (\forall x\in A.\ \langle x, M\rangle \in r) \) using HasAmaximum_def
fix \( M1 \) \( M2 \)
assume A2: \( M1 \in A \wedge (\forall x\in A.\ \langle x, M1\rangle \in r) \), \( M2 \in A \wedge (\forall x\in A.\ \langle x, M2\rangle \in r) \)
then have \( \langle M1,M2\rangle \in r \), \( \langle M2,M1\rangle \in r \)
with A1 show \( M1=M2 \) by (rule Fol1_L4 )
qed
For antisymmetric relations minimum of a set is unique if it exists.
lemma Order_ZF_4_L2:
assumes A1: \( \text{antisym}(r) \) and A2: \( \text{HasAminimum}(r,A) \)
shows \( \exists !m.\ m\in A \wedge (\forall x\in A.\ \langle m,x\rangle \in r) \)proof from A2 show \( \exists m.\ m \in A \wedge (\forall x\in A.\ \langle m, x\rangle \in r) \) using HasAminimum_def
fix \( m1 \) \( m2 \)
assume A2: \( m1 \in A \wedge (\forall x\in A.\ \langle m1, x\rangle \in r) \), \( m2 \in A \wedge (\forall x\in A.\ \langle m2, x\rangle \in r) \)
then have \( \langle m1,m2\rangle \in r \), \( \langle m2,m1\rangle \in r \)
with A1 show \( m1=m2 \) by (rule Fol1_L4 )
qed
Maximum of a set has desired properties.
lemma Order_ZF_4_L3:
assumes A1: \( \text{antisym}(r) \) and A2: \( \text{HasAmaximum}(r,A) \)
shows \( \text{Maximum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r \)proof let \( Max = \text{The } M.\ M\in A \wedge (\forall x\in A.\ \langle x,M\rangle \in r) \)
from A1, A2 have \( \exists !M.\ M\in A \wedge (\forall x\in A.\ \langle x,M\rangle \in r) \) by (rule Order_ZF_4_L1 )
then have \( Max \in A \wedge (\forall x\in A.\ \langle x,Max\rangle \in r) \) by (rule theI )
then show \( \text{Maximum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r \) using Maximum_def
qed
Minimum of a set has desired properties.
lemma Order_ZF_4_L4:
assumes A1: \( \text{antisym}(r) \) and A2: \( \text{HasAminimum}(r,A) \)
shows \( \text{Minimum}(r,A) \in A \), \( \forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r \)proof let \( Min = \text{The } m.\ m\in A \wedge (\forall x\in A.\ \langle m,x\rangle \in r) \)
from A1, A2 have \( \exists !m.\ m\in A \wedge (\forall x\in A.\ \langle m,x\rangle \in r) \) by (rule Order_ZF_4_L2 )
then have \( Min \in A \wedge (\forall x\in A.\ \langle Min,x\rangle \in r) \) by (rule theI )
then show \( \text{Minimum}(r,A) \in A \), \( \forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r \) using Minimum_def
qed
For total and transitive relations a union a of two sets that have maxima has a maximum.
lemma Order_ZF_4_L5:
assumes A1: \( r \text{ is total on } (A\cup B) \) and A2: \( \text{trans}(r) \) and A3: \( \text{HasAmaximum}(r,A) \), \( \text{HasAmaximum}(r,B) \)
shows \( \text{HasAmaximum}(r,A\cup B) \)proof from A3 obtain \( M \) \( K \) where D1: \( M\in A \wedge (\forall x\in A.\ \langle x,M\rangle \in r) \), \( K\in B \wedge (\forall x\in B.\ \langle x,K\rangle \in r) \) using HasAmaximum_def
let \( L = \text{GreaterOf}(r,M,K) \)
from D1 have T1: \( M \in A\cup B \), \( K \in A\cup B \), \( \forall x\in A.\ \langle x,M\rangle \in r \), \( \forall x\in B.\ \langle x,K\rangle \in r \)
with A1, A2 have \( \forall x\in A\cup B.\ \langle x,L\rangle \in r \) by (rule Order_ZF_3_L2B )
moreover
qed
from T1 have \( L \in A\cup B \) using GreaterOf_def, IsTotal_def
ultimately show \( \text{HasAmaximum}(r,A\cup B) \) using HasAmaximum_def
For total and transitive relations A union a of two sets that have minima has a minimum.
lemma Order_ZF_4_L6:
assumes A1: \( r \text{ is total on } (A\cup B) \) and A2: \( \text{trans}(r) \) and A3: \( \text{HasAminimum}(r,A) \), \( \text{HasAminimum}(r,B) \)
shows \( \text{HasAminimum}(r,A\cup B) \)proof from A3 obtain \( m \) \( k \) where D1: \( m\in A \wedge (\forall x\in A.\ \langle m,x\rangle \in r) \), \( k\in B \wedge (\forall x\in B.\ \langle k,x\rangle \in r) \) using HasAminimum_def
let \( l = \text{SmallerOf}(r,m,k) \)
from D1 have T1: \( m \in A\cup B \), \( k \in A\cup B \), \( \forall x\in A.\ \langle m,x\rangle \in r \), \( \forall x\in B.\ \langle k,x\rangle \in r \)
with A1, A2 have \( \forall x\in A\cup B.\ \langle l,x\rangle \in r \) by (rule Order_ZF_3_L5B )
moreover
qed
from T1 have \( l \in A\cup B \) using SmallerOf_def, IsTotal_def
ultimately show \( \text{HasAminimum}(r,A\cup B) \) using HasAminimum_def
Set that has a maximum is bounded above.
lemma Order_ZF_4_L7:
assumes \( \text{HasAmaximum}(r,A) \)
shows \( \text{IsBoundedAbove}(A,r) \) using assms, HasAmaximum_def, IsBoundedAbove_defSet that has a minimum is bounded below.
lemma Order_ZF_4_L8A:
assumes \( \text{HasAminimum}(r,A) \)
shows \( \text{IsBoundedBelow}(A,r) \) using assms, HasAminimum_def, IsBoundedBelow_defFor reflexive relations singletons have a minimum and maximum.
lemma Order_ZF_4_L8:
assumes \( \text{refl}(X,r) \) and \( a\in X \)
shows \( \text{HasAmaximum}(r,\{a\}) \), \( \text{HasAminimum}(r,\{a\}) \) using assms, refl_def, HasAmaximum_def, HasAminimum_defFor total and transitive relations if we add an element to a set that has a maximum, the set still has a maximum.
lemma Order_ZF_4_L9:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( A\subseteq X \) and A4: \( a\in X \) and A5: \( \text{HasAmaximum}(r,A) \)
shows \( \text{HasAmaximum}(r,A\cup \{a\}) \)proof from A3, A4 have \( A\cup \{a\} \subseteq X \)
with A1 have \( r \text{ is total on } (A\cup \{a\}) \) using Order_ZF_1_L4
moreover
qed
from A1, A2, A4, A5 have \( \text{trans}(r) \), \( \text{HasAmaximum}(r,A) \)
moreover from A1, A4 have \( \text{HasAmaximum}(r,\{a\}) \) using total_is_refl, Order_ZF_4_L8
ultimately show \( \text{HasAmaximum}(r,A\cup \{a\}) \) by (rule Order_ZF_4_L5 )
For total and transitive relations if we add an element to a set that has a minimum, the set still has a minimum.
lemma Order_ZF_4_L10:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( A\subseteq X \) and A4: \( a\in X \) and A5: \( \text{HasAminimum}(r,A) \)
shows \( \text{HasAminimum}(r,A\cup \{a\}) \)proof from A3, A4 have \( A\cup \{a\} \subseteq X \)
with A1 have \( r \text{ is total on } (A\cup \{a\}) \) using Order_ZF_1_L4
moreover
qed
from A1, A2, A4, A5 have \( \text{trans}(r) \), \( \text{HasAminimum}(r,A) \)
moreover from A1, A4 have \( \text{HasAminimum}(r,\{a\}) \) using total_is_refl, Order_ZF_4_L8
ultimately show \( \text{HasAminimum}(r,A\cup \{a\}) \) by (rule Order_ZF_4_L6 )
If the order relation has a property that every nonempty bounded set attains a minimum (for example integers are like that), then every nonempty set bounded below attains a minimum.
lemma Order_ZF_4_L11:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( r \subseteq X\times X \) and A4: \( \forall A.\ \text{IsBounded}(A,r) \wedge A\neq 0 \longrightarrow \text{HasAminimum}(r,A) \) and A5: \( B\neq 0 \) and A6: \( \text{IsBoundedBelow}(B,r) \)
shows \( \text{HasAminimum}(r,B) \)proof from A5 obtain \( b \) where T: \( b\in B \)
let \( L = \{x\in B.\ \langle x,b\rangle \in r\} \)
from A3, A6, T have T1: \( b\in X \) using Order_ZF_3_L1B
with A1, T have T2: \( b \in L \) using total_is_refl, refl_def
then have \( L \neq 0 \)
moreover
have \( \text{IsBounded}(L,r) \)proof
ultimately have \( \text{IsBounded}(L,r) \wedge L \neq 0 \)
have \( L \subseteq B \)
with A6 have \( \text{IsBoundedBelow}(L,r) \) using Order_ZF_3_L12
moreover
qed
have \( \text{IsBoundedAbove}(L,r) \) by (rule Order_ZF_3_L15 )
ultimately have \( \text{IsBoundedAbove}(L,r) \wedge \text{IsBoundedBelow}(L,r) \)
then show \( \text{IsBounded}(L,r) \) using IsBounded_def
with A4 have \( \text{HasAminimum}(r,L) \)
then obtain \( m \) where I: \( m\in L \) and II: \( \forall x\in L.\ \langle m,x\rangle \in r \) using HasAminimum_def
then have III: \( \langle m,b\rangle \in r \)
from I have \( m\in B \)
moreover
qed
have \( \forall x\in B.\ \langle m,x\rangle \in r \)proof
ultimately show \( \text{HasAminimum}(r,B) \) using HasAminimum_def
fix \( x \)
assume A7: \( x\in B \)
from A3, A6 have \( B\subseteq X \) using Order_ZF_3_L1B
with A1, A7, T1 have \( x \in L \cup \{x\in B.\ \langle b,x\rangle \in r\} \) using Order_ZF_1_L5
then have \( x\in L \vee \langle b,x\rangle \in r \)
moreover {
}
moreover {
}
ultimately show \( \langle m,x\rangle \in r \)
qed
assume \( x\in L \)
with II have \( \langle m,x\rangle \in r \)
assume \( \langle b,x\rangle \in r \)
with A2, III have \( \text{trans}(r) \) and \( \langle m,b\rangle \in r \wedge \langle b,x\rangle \in r \)
then have \( \langle m,x\rangle \in r \) by (rule Fol1_L3 )
A dual to Order_ZF_4_L11: If the order relation has a property that every nonempty bounded set attains a maximum (for example integers are like that), then every nonempty set bounded above attains a maximum.
lemma Order_ZF_4_L11A:
assumes A1: \( r \text{ is total on } X \) and A2: \( \text{trans}(r) \) and A3: \( r \subseteq X\times X \) and A4: \( \forall A.\ \text{IsBounded}(A,r) \wedge A\neq 0 \longrightarrow \text{HasAmaximum}(r,A) \) and A5: \( B\neq 0 \) and A6: \( \text{IsBoundedAbove}(B,r) \)
shows \( \text{HasAmaximum}(r,B) \)proof from A5 obtain \( b \) where T: \( b\in B \)
let \( U = \{x\in B.\ \langle b,x\rangle \in r\} \)
from A3, A6, T have T1: \( b\in X \) using Order_ZF_3_L1A
with A1, T have T2: \( b \in U \) using total_is_refl, refl_def
then have \( U \neq 0 \)
moreover
have \( \text{IsBounded}(U,r) \)proof
ultimately have \( \text{IsBounded}(U,r) \wedge U \neq 0 \)
have \( U \subseteq B \)
with A6 have \( \text{IsBoundedAbove}(U,r) \) using Order_ZF_3_L13
moreover
qed
have \( \text{IsBoundedBelow}(U,r) \) using IsBoundedBelow_def
ultimately have \( \text{IsBoundedAbove}(U,r) \wedge \text{IsBoundedBelow}(U,r) \)
then show \( \text{IsBounded}(U,r) \) using IsBounded_def
with A4 have \( \text{HasAmaximum}(r,U) \)
then obtain \( m \) where I: \( m\in U \) and II: \( \forall x\in U.\ \langle x,m\rangle \in r \) using HasAmaximum_def
then have III: \( \langle b,m\rangle \in r \)
from I have \( m\in B \)
moreover
qed
have \( \forall x\in B.\ \langle x,m\rangle \in r \)proof
ultimately show \( \text{HasAmaximum}(r,B) \) using HasAmaximum_def
fix \( x \)
assume A7: \( x\in B \)
from A3, A6 have \( B\subseteq X \) using Order_ZF_3_L1A
with A1, A7, T1 have \( x \in \{x\in B.\ \langle x,b\rangle \in r\} \cup U \) using Order_ZF_1_L5
then have \( x\in U \vee \langle x,b\rangle \in r \)
moreover {
}
moreover {
}
ultimately show \( \langle x,m\rangle \in r \)
qed
assume \( x\in U \)
with II have \( \langle x,m\rangle \in r \)
assume \( \langle x,b\rangle \in r \)
with A2, III have \( \text{trans}(r) \) and \( \langle x,b\rangle \in r \wedge \langle b,m\rangle \in r \)
then have \( \langle x,m\rangle \in r \) by (rule Fol1_L3 )
If a set has a minimum and \(L\) is less or equal than all elements of the set, then \(L\) is less or equal than the minimum.
lemma Order_ZF_4_L12:
assumes \( \text{antisym}(r) \) and \( \text{HasAminimum}(r,A) \) and \( \forall a\in A.\ \langle L,a\rangle \in r \)
shows \( \langle L, \text{Minimum}(r,A)\rangle \in r \) using assms, Order_ZF_4_L4If a set has a maximum and all its elements are less or equal than \(M\), then the maximum of the set is less or equal than \(M\).
lemma Order_ZF_4_L13:
assumes \( \text{antisym}(r) \) and \( \text{HasAmaximum}(r,A) \) and \( \forall a\in A.\ \langle a,M\rangle \in r \)
shows \( \langle \text{Maximum}(r,A),M\rangle \in r \) using assms, Order_ZF_4_L3If an element belongs to a set and is greater or equal than all elements of that set, then it is the maximum of that set.
lemma Order_ZF_4_L14:
assumes A1: \( \text{antisym}(r) \) and A2: \( M \in A \) and A3: \( \forall a\in A.\ \langle a,M\rangle \in r \)
shows \( \text{Maximum}(r,A) = M \)proof from A2, A3 have I: \( \text{HasAmaximum}(r,A) \) using HasAmaximum_def
with A1 have \( \exists !M.\ M\in A \wedge (\forall x\in A.\ \langle x,M\rangle \in r) \) using Order_ZF_4_L1
moreover
qed
from A2, A3 have \( M\in A \wedge (\forall x\in A.\ \langle x,M\rangle \in r) \)
moreover from A1, I have \( \text{Maximum}(r,A) \in A \wedge (\forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r) \) using Order_ZF_4_L3
ultimately show \( \text{Maximum}(r,A) = M \)
If an element belongs to a set and is less or equal than all elements of that set, then it is the minimum of that set.
lemma Order_ZF_4_L15:
assumes A1: \( \text{antisym}(r) \) and A2: \( m \in A \) and A3: \( \forall a\in A.\ \langle m,a\rangle \in r \)
shows \( \text{Minimum}(r,A) = m \)proof from A2, A3 have I: \( \text{HasAminimum}(r,A) \) using HasAminimum_def
with A1 have \( \exists !m.\ m\in A \wedge (\forall x\in A.\ \langle m,x\rangle \in r) \) using Order_ZF_4_L2
moreover
qed
from A2, A3 have \( m\in A \wedge (\forall x\in A.\ \langle m,x\rangle \in r) \)
moreover from A1, I have \( \text{Minimum}(r,A) \in A \wedge (\forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r) \) using Order_ZF_4_L4
ultimately show \( \text{Minimum}(r,A) = m \)
If a set does not have a maximum, then for any its element we can find one that is (strictly) greater.
lemma Order_ZF_4_L16:
assumes A1: \( \text{antisym}(r) \) and A2: \( r \text{ is total on } X \) and A3: \( A\subseteq X \) and A4: \( \neg \text{HasAmaximum}(r,A) \) and A5: \( x\in A \)
shows \( \exists y\in A.\ \langle x,y\rangle \in r \wedge y\neq x \)proof{
}
assume A6: \( \forall y\in A.\ \langle x,y\rangle \notin r \vee y=x \)
have \( \forall y\in A.\ \langle y,x\rangle \in r \)proof
fix \( y \)
assume A7: \( y\in A \)
with A6 have \( \langle x,y\rangle \notin r \vee y=x \)
with A2, A3, A5, A7 show \( \langle y,x\rangle \in r \) using IsTotal_def, Order_ZF_1_L1
qed
with A5 have \( \exists x\in A.\ \forall y\in A.\ \langle y,x\rangle \in r \)
with A4 have \( False \) using HasAmaximum_def
then show \( \exists y\in A.\ \langle x,y\rangle \in r \wedge y\neq x \)
qed
Supremum and Infimum
In this section we consider the notions of supremum and infimum a set.
Elements of the set of upper bounds are indeed upper bounds. Isabelle also thinks it is obvious.
lemma Order_ZF_5_L1:
assumes \( u \in (\bigcap a\in A.\ r\{a\}) \) and \( a\in A \)
shows \( \langle a,u\rangle \in r \) using assmsElements of the set of lower bounds are indeed lower bounds. Isabelle also thinks it is obvious.
lemma Order_ZF_5_L2:
assumes \( l \in (\bigcap a\in A.\ r^{-1}\{a\}) \) and \( a\in A \)
shows \( \langle l,a\rangle \in r \) using assmsIf the set of upper bounds has a minimum, then the supremum is less or equal than any upper bound. We can probably do away with the assumption that \(A\) is not empty, (ab)using the fact that intersection over an empty family is defined in Isabelle to be empty. This lemma is obsolete and will be removed in the future. Use sup_leq_up_bnd instead.
lemma Order_ZF_5_L3:
assumes A1: \( \text{antisym}(r) \) and A2: \( A\neq 0 \) and A3: \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \) and A4: \( \forall a\in A.\ \langle a,u\rangle \in r \)
shows \( \langle \text{Supremum}(r,A),u\rangle \in r \)proof let \( U = \bigcap a\in A.\ r\{a\} \)
from A4 have \( \forall a\in A.\ u \in r\{a\} \) using image_singleton_iff
with A2 have \( u\in U \)
with A1, A3 show \( \langle \text{Supremum}(r,A),u\rangle \in r \) using Order_ZF_4_L4, Supremum_def
qed
Supremum is less or equal than any upper bound.
lemma sup_leq_up_bnd:
assumes \( \text{antisym}(r) \), \( \text{HasAsupremum}(r,A) \), \( \forall a\in A.\ \langle a,u\rangle \in r \)
shows \( \langle \text{Supremum}(r,A),u\rangle \in r \)proof let \( U = \bigcap a\in A.\ r\{a\} \)
from assms(3) have \( \forall a\in A.\ u \in r\{a\} \) using image_singleton_iff
with assms(2) have \( u\in U \) using set_sup_not_empty
with assms(1,2) show \( \langle \text{Supremum}(r,A),u\rangle \in r \) unfolding HasAsupremum_def, Supremum_def using Order_ZF_4_L4
qed
Infimum is greater or equal than any lower bound. This lemma is obsolete and will be removed. Use inf_geq_lo_bnd instead.
lemma Order_ZF_5_L4:
assumes A1: \( \text{antisym}(r) \) and A2: \( A\neq 0 \) and A3: \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \) and A4: \( \forall a\in A.\ \langle l,a\rangle \in r \)
shows \( \langle l, \text{Infimum}(r,A)\rangle \in r \)proof let \( L = \bigcap a\in A.\ r^{-1}\{a\} \)
from A4 have \( \forall a\in A.\ l \in r^{-1}\{a\} \) using vimage_singleton_iff
with A2 have \( l\in L \)
with A1, A3 show \( \langle l, \text{Infimum}(r,A)\rangle \in r \) using Order_ZF_4_L3, Infimum_def
qed
Infimum is greater or equal than any upper bound.
lemma inf_geq_lo_bnd:
assumes \( \text{antisym}(r) \), \( \text{HasAnInfimum}(r,A) \), \( \forall a\in A.\ \langle u,a\rangle \in r \)
shows \( \langle u, \text{Infimum}(r,A)\rangle \in r \)proof let \( U = \bigcap a\in A.\ r^{-1}\{a\} \)
from assms(3) have \( \forall a\in A.\ u \in r^{-1}\{a\} \) using vimage_singleton_iff
with assms(2) have \( u\in U \) using set_inf_not_empty
with assms(1,2) show \( \langle u, \text{Infimum}(r,A)\rangle \in r \) unfolding HasAnInfimum_def, Infimum_def using Order_ZF_4_L3
qed
If \(z\) is an upper bound for \(A\) and is less or equal than any other upper bound, then \(z\) is the supremum of \(A\).
lemma Order_ZF_5_L5:
assumes A1: \( \text{antisym}(r) \) and A2: \( A\neq 0 \) and A3: \( \forall x\in A.\ \langle x,z\rangle \in r \) and A4: \( \forall y.\ (\forall x\in A.\ \langle x,y\rangle \in r) \longrightarrow \langle z,y\rangle \in r \)
shows \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \), \( z = \text{Supremum}(r,A) \)proof let \( B = \bigcap a\in A.\ r\{a\} \)
from A2, A3, A4 have I: \( z \in B \), \( \forall y\in B.\ \langle z,y\rangle \in r \)
then show \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \) using HasAminimum_def
from A1, I show \( z = \text{Supremum}(r,A) \) using Order_ZF_4_L15, Supremum_def
qed
The dual theorem to Order_ZF_5_L5: if \(z\) is an lower bound for \(A\) and is greater or equal than any other lower bound, then \(z\) is the infimum of \(A\).
lemma inf_glb:
assumes \( \text{antisym}(r) \), \( A\neq 0 \), \( \forall x\in A.\ \langle z,x\rangle \in r \), \( \forall y.\ (\forall x\in A.\ \langle y,x\rangle \in r) \longrightarrow \langle y,z\rangle \in r \)
shows \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \), \( z = \text{Infimum}(r,A) \)proof let \( B = \bigcap a\in A.\ r^{-1}\{a\} \)
from assms(2,3,4) have I: \( z \in B \), \( \forall y\in B.\ \langle y,z\rangle \in r \)
then show \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \) unfolding HasAmaximum_def
from assms(1), I show \( z = \text{Infimum}(r,A) \) using Order_ZF_4_L14, Infimum_def
qed
Supremum and infimum of a singleton is the element.
lemma sup_inf_singl:
assumes \( \text{antisym}(r) \), \( \text{refl}(X,r) \), \( z\in X \)
shows \( \text{HasAsupremum}(r,\{z\}) \), \( \text{Supremum}(r,\{z\}) = z \) and \( \text{HasAnInfimum}(r,\{z\}) \), \( \text{Infimum}(r,\{z\}) = z \)proof from assms show \( \text{Supremum}(r,\{z\}) = z \) and \( \text{Infimum}(r,\{z\}) = z \) using inf_glb, Order_ZF_5_L5 unfolding refl_def
from assms show \( \text{HasAsupremum}(r,\{z\}) \) using Order_ZF_5_L5 unfolding HasAsupremum_def, refl_def
from assms show \( \text{HasAnInfimum}(r,\{z\}) \) using inf_glb unfolding HasAnInfimum_def, refl_def
qed
If a set has a maximum, then the maximum is the supremum. This lemma is obsolete, use max_is_sup instead.
lemma Order_ZF_5_L6:
assumes A1: \( \text{antisym}(r) \) and A2: \( A\neq 0 \) and A3: \( \text{HasAmaximum}(r,A) \)
shows \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \), \( \text{Maximum}(r,A) = \text{Supremum}(r,A) \)proof let \( M = \text{Maximum}(r,A) \)
from A1, A3 have I: \( M \in A \) and II: \( \forall x\in A.\ \langle x,M\rangle \in r \) using Order_ZF_4_L3
from I have III: \( \forall y.\ (\forall x\in A.\ \langle x,y\rangle \in r) \longrightarrow \langle M,y\rangle \in r \)
with A1, A2, II show \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \) by (rule Order_ZF_5_L5 )
from A1, A2, II, III show \( M = \text{Supremum}(r,A) \) by (rule Order_ZF_5_L5 )
qed
Another version of Order_ZF_5_L6 that: if a sat has a maximum then it has a supremum and the maximum is the supremum.
lemma max_is_sup:
assumes \( \text{antisym}(r) \), \( A\neq 0 \), \( \text{HasAmaximum}(r,A) \)
shows \( \text{HasAsupremum}(r,A) \) and \( \text{Maximum}(r,A) = \text{Supremum}(r,A) \)proof let \( M = \text{Maximum}(r,A) \)
from assms(1,3) have \( M \in A \) and I: \( \forall x\in A.\ \langle x,M\rangle \in r \) using Order_ZF_4_L3
with assms(1,2) have \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \) using Order_ZF_5_L5(1)
then show \( \text{HasAsupremum}(r,A) \) unfolding HasAsupremum_def
from assms(1,2), \( M \in A \), I show \( M = \text{Supremum}(r,A) \) using Order_ZF_5_L5(2)
qed
Minimum is the infimum if it exists.
lemma min_is_inf:
assumes \( \text{antisym}(r) \), \( A\neq 0 \), \( \text{HasAminimum}(r,A) \)
shows \( \text{HasAnInfimum}(r,A) \) and \( \text{Minimum}(r,A) = \text{Infimum}(r,A) \)proof let \( M = \text{Minimum}(r,A) \)
from assms(1,3) have \( M\in A \) and I: \( \forall x\in A.\ \langle M,x\rangle \in r \) using Order_ZF_4_L4
with assms(1,2) have \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \) using inf_glb(1)
then show \( \text{HasAnInfimum}(r,A) \) unfolding HasAnInfimum_def
from assms(1,2), \( M \in A \), I show \( M = \text{Infimum}(r,A) \) using inf_glb(2)
qed
For reflexive and total relations two-element set has a minimum and a maximum.
lemma min_max_two_el:
assumes \( r \text{ is total on } X \), \( x\in X \), \( y\in X \)
shows \( \text{HasAminimum}(r,\{x,y\}) \) and \( \text{HasAmaximum}(r,\{x,y\}) \) using assms unfolding IsTotal_def, HasAminimum_def, HasAmaximum_defFor antisymmetric, reflexive and total relations two-element set has a supremum and infimum.
lemma inf_sup_two_el:
assumes \( \text{antisym}(r) \), \( r \text{ is total on } X \), \( x\in X \), \( y\in X \)
shows \( \text{HasAnInfimum}(r,\{x,y\}) \), \( \text{Minimum}(r,\{x,y\}) = \text{Infimum}(r,\{x,y\}) \), \( \text{HasAsupremum}(r,\{x,y\}) \), \( \text{Maximum}(r,\{x,y\}) = \text{Supremum}(r,\{x,y\}) \) using assms, min_max_two_el, max_is_sup, min_is_infA sufficient condition for the supremum to be in the space.
lemma sup_in_space:
assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)
shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \)proof from assms(3) have \( A\neq 0 \) using set_sup_not_empty unfolding HasAsupremum_def
then obtain \( a \) where \( a\in A \)
with assms(1,2,3) show \( \text{Supremum}(r,A) \in X \) unfolding Supremum_def using Order_ZF_4_L4, Order_ZF_5_L1
from assms(2,3) show \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \) unfolding Supremum_def using Order_ZF_4_L4
qed
A sufficient condition for the infimum to be in the space.
lemma inf_in_space:
assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)
shows \( \text{Infimum}(r,A) \in X \) and \( \forall x\in A.\ \langle \text{Infimum}(r,A),x\rangle \in r \)proof from assms(3) have \( A\neq 0 \) using set_inf_not_empty unfolding HasAnInfimum_def
then obtain \( a \) where \( a\in A \)
with assms(1,2,3) show \( \text{Infimum}(r,A) \in X \) unfolding Infimum_def using Order_ZF_4_L3, Order_ZF_5_L1
from assms(2,3) show \( \forall x\in A.\ \langle \text{Infimum}(r,A),x\rangle \in r \) unfolding Infimum_def using Order_ZF_4_L3
qed
Properties of supremum of a set for complete relations.
lemma Order_ZF_5_L7:
assumes A1: \( r \subseteq X\times X \) and A2: \( \text{antisym}(r) \) and A3: \( r \text{ is complete } \) and A4: \( A\neq 0 \) and A5: \( \exists x\in X.\ \forall y\in A.\ \langle y,x\rangle \in r \)
shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \)proof from A3, A4, A5 have \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \) unfolding IsBoundedAbove_def, IsComplete_def
with A1, A2 show \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \) using sup_in_space
qed
Infimum of the set of infima of a collection of sets is infimum of the union.
lemma inf_inf:
assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{trans}(r) \), \( \forall T\in \mathcal{T} .\ \text{HasAnInfimum}(r,T) \), \( \text{HasAnInfimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) \)
shows \( \text{HasAnInfimum}(r,\bigcup \mathcal{T} ) \) and \( \text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) = \text{Infimum}(r,\bigcup \mathcal{T} ) \)proof let \( i = \text{Infimum}(r,\{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}) \)
note assms(2)
moreover
from assms(4,5) have \( \bigcup \mathcal{T} \neq 0 \) using set_inf_not_empty
moreover have \( \forall T\in \mathcal{T} .\ \forall t\in T.\ \langle i,t\rangle \in r \)proof
{
}
fix \( T \) \( t \)
assume \( T\in \mathcal{T} \), \( t\in T \)
with assms(1,2,4) have \( \langle \text{Infimum}(r,T),t\rangle \in r \) unfolding HasAnInfimum_def using inf_in_space(2)
moreover
from assms(1,2,5), \( T\in \mathcal{T} \) have \( \langle i, \text{Infimum}(r,T)\rangle \in r \) unfolding HasAnInfimum_def using inf_in_space(2)
moreover note assms(3)
ultimately have \( \langle i,t\rangle \in r \) unfolding trans_def
thus \( thesis \)
qed
hence I: \( \forall t\in \bigcup \mathcal{T} .\ \langle i,t\rangle \in r \)
moreover have J: \( \forall y.\ (\forall x\in \bigcup \mathcal{T} .\ \langle y,x\rangle \in r) \longrightarrow \langle y,i\rangle \in r \)proof
ultimately have \( \text{HasAmaximum}(r,\bigcap a\in \bigcup \mathcal{T} .\ r^{-1}\{a\}) \) by (rule inf_glb )
{
}
fix \( y \) \( x \)
assume A: \( \forall x\in \bigcup \mathcal{T} .\ \langle y,x\rangle \in r \)
with assms(2,4) have \( \forall a\in \{ \text{Infimum}(r,T).\ T\in \mathcal{T} \}.\ \langle y,a\rangle \in r \) using inf_geq_lo_bnd
with assms(2,5) have \( \langle y,i\rangle \in r \) by (rule inf_geq_lo_bnd )
thus \( thesis \)
qed
then show \( \text{HasAnInfimum}(r,\bigcup \mathcal{T} ) \) unfolding HasAnInfimum_def
from assms(2), \( \bigcup \mathcal{T} \neq 0 \), I, J show \( i = \text{Infimum}(r,\bigcup \mathcal{T} ) \) by (rule inf_glb )
qed
Supremum of the set of suprema of a collection of sets is supremum of the union.
lemma sup_sup:
assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{trans}(r) \), \( \forall T\in \mathcal{T} .\ \text{HasAsupremum}(r,T) \), \( \text{HasAsupremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) \)
shows \( \text{HasAsupremum}(r,\bigcup \mathcal{T} ) \) and \( \text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) = \text{Supremum}(r,\bigcup \mathcal{T} ) \)proof let \( s = \text{Supremum}(r,\{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}) \)
note assms(2)
moreover
from assms(4,5) have \( \bigcup \mathcal{T} \neq 0 \) using set_sup_not_empty
moreover have \( \forall T\in \mathcal{T} .\ \forall t\in T.\ \langle t,s\rangle \in r \)proof
{
}
fix \( T \) \( t \)
assume \( T\in \mathcal{T} \), \( t\in T \)
with assms(1,2,4) have \( \langle t, \text{Supremum}(r,T)\rangle \in r \) unfolding HasAsupremum_def using sup_in_space(2)
moreover
from assms(1,2,5), \( T\in \mathcal{T} \) have \( \langle \text{Supremum}(r,T),s\rangle \in r \) unfolding HasAsupremum_def using sup_in_space(2)
moreover note assms(3)
ultimately have \( \langle t,s\rangle \in r \) unfolding trans_def
thus \( thesis \)
qed
hence I: \( \forall t\in \bigcup \mathcal{T} .\ \langle t,s\rangle \in r \)
moreover have J: \( \forall y.\ (\forall x\in \bigcup \mathcal{T} .\ \langle x,y\rangle \in r) \longrightarrow \langle s,y\rangle \in r \)proof
ultimately have \( \text{HasAminimum}(r,\bigcap a\in \bigcup \mathcal{T} .\ r\{a\}) \) by (rule Order_ZF_5_L5 )
{
}
fix \( y \) \( x \)
assume A: \( \forall x\in \bigcup \mathcal{T} .\ \langle x,y\rangle \in r \)
with assms(2,4) have \( \forall a\in \{ \text{Supremum}(r,T).\ T\in \mathcal{T} \}.\ \langle a,y\rangle \in r \) using sup_leq_up_bnd
with assms(2,5) have \( \langle s,y\rangle \in r \) by (rule sup_leq_up_bnd )
thus \( thesis \)
qed
then show \( \text{HasAsupremum}(r,\bigcup \mathcal{T} ) \) unfolding HasAsupremum_def
from assms(2), \( \bigcup \mathcal{T} \neq 0 \), I, J show \( s = \text{Supremum}(r,\bigcup \mathcal{T} ) \) by (rule Order_ZF_5_L5 )
qed
If the relation is a linear order then for any element \(y\) smaller than the supremum of a set we can find one element of the set that is greater than \(y\).
lemma Order_ZF_5_L8:
assumes A1: \( r \subseteq X\times X \) and A2: \( \text{IsLinOrder}(X,r) \) and A3: \( r \text{ is complete } \) and A4: \( A\subseteq X \), \( A\neq 0 \) and A5: \( \exists x\in X.\ \forall y\in A.\ \langle y,x\rangle \in r \) and A6: \( \langle y, \text{Supremum}(r,A)\rangle \in r \), \( y \neq \text{Supremum}(r,A) \)
shows \( \exists z\in A.\ \langle y,z\rangle \in r \wedge y \neq z \)proof from A2 have I: \( \text{antisym}(r) \) and II: \( \text{trans}(r) \) and III: \( r \text{ is total on } X \) using IsLinOrder_def
from A1, A6 have T1: \( y\in X \)
{
assume A7: \( \forall z \in A.\ \langle y,z\rangle \notin r \vee y=z \)
from A4, I have \( \text{antisym}(r) \) and \( A\neq 0 \)
moreover
have \( \forall x\in A.\ \langle x,y\rangle \in r \)proof
moreover fix \( x \)
assume A8: \( x\in A \)
with A4 have T2: \( x\in X \)
from A7, A8 have \( \langle y,x\rangle \notin r \vee y=x \)
with III, T1, T2 show \( \langle x,y\rangle \in r \) using IsTotal_def, total_is_refl, refl_def
qed
have \( \forall u.\ (\forall x\in A.\ \langle x,u\rangle \in r) \longrightarrow \langle y,u\rangle \in r \)proof
ultimately have \( y = \text{Supremum}(r,A) \) by (rule Order_ZF_5_L5 )
{
}
fix \( u \)
assume A9: \( \forall x\in A.\ \langle x,u\rangle \in r \)
from A4, A5 have \( \text{IsBoundedAbove}(A,r) \) and \( A\neq 0 \) using IsBoundedAbove_def
with A3, A4, A6, I, A9 have \( \langle y, \text{Supremum}(r,A)\rangle \in r \wedge \langle \text{Supremum}(r,A),u\rangle \in r \) using IsComplete_def, Order_ZF_5_L3
with II have \( \langle y,u\rangle \in r \) by (rule Fol1_L3 )
then show \( \forall u.\ (\forall x\in A.\ \langle x,u\rangle \in r) \longrightarrow \langle y,u\rangle \in r \)
qed
with A6 have \( False \)
then show \( \exists z\in A.\ \langle y,z\rangle \in r \wedge y \neq z \)
qed
Strict versions of order relations
One of the problems with translating formalized mathematics from Metamath to IsarMathLib is that Metamath uses strict orders (of the \(<\) type) while in IsarMathLib we mostly use nonstrict orders (of the \(\leq\) type). This doesn't really make any difference, but is annoying as we have to prove many theorems twice. In this section we prove some theorems to make it easier to translate the statements about strict orders to statements about the corresponding non-strict order and vice versa.
We define a strict version of a relation by removing the \(y=x\) line from the relation.
definition
\( \text{StrictVersion}(r) \equiv r - \{\langle x,x\rangle .\ x \in domain(r)\} \)
A reformulation of the definition of a strict version of an order.
lemma def_of_strict_ver:
shows \( \langle x,y\rangle \in \text{StrictVersion}(r) \longleftrightarrow \langle x,y\rangle \in r \wedge x\neq y \) using StrictVersion_def, domain_defThe next lemma is about the strict version of an antisymmetric relation.
lemma strict_of_antisym:
assumes A1: \( \text{antisym}(r) \) and A2: \( \langle a,b\rangle \in \text{StrictVersion}(r) \)
shows \( \langle b,a\rangle \notin \text{StrictVersion}(r) \)proof{
}
assume A3: \( \langle b,a\rangle \in \text{StrictVersion}(r) \)
with A2 have \( \langle a,b\rangle \in r \) and \( \langle b,a\rangle \in r \) using def_of_strict_ver
with A1 have \( a=b \) by (rule Fol1_L4 )
with A2 have \( False \) using def_of_strict_ver
then show \( \langle b,a\rangle \notin \text{StrictVersion}(r) \)
qed
The strict version of totality.
lemma strict_of_tot:
assumes \( r \text{ is total on } X \) and \( a\in X \), \( b\in X \), \( a\neq b \)
shows \( \langle a,b\rangle \in \text{StrictVersion}(r) \vee \langle b,a\rangle \in \text{StrictVersion}(r) \) using assms, IsTotal_def, def_of_strict_verA trichotomy law for the strict version of a total and antisymmetric relation. It is kind of interesting that one does not need the full linear order for this.
lemma strict_ans_tot_trich:
assumes A1: \( \text{antisym}(r) \) and A2: \( r \text{ is total on } X \) and A3: \( a\in X \), \( b\in X \) and A4: \( s = \text{StrictVersion}(r) \)
shows \( \text{Exactly_1_of_3_holds} (\langle a,b\rangle \in s, a=b,\langle b,a\rangle \in s) \)proof let \( p = \langle a,b\rangle \in s \)
let \( q = a=b \)
let \( r = \langle b,a\rangle \in s \)
from A2, A3, A4 have \( p \vee q \vee r \) using strict_of_tot
moreover
qed
from A1, A4 have \( p \longrightarrow \neg q \wedge \neg r \) using def_of_strict_ver, strict_of_antisym
moreover from A4 have \( q \longrightarrow \neg p \wedge \neg r \) using def_of_strict_ver
moreover from A1, A4 have \( r \longrightarrow \neg p \wedge \neg q \) using def_of_strict_ver, strict_of_antisym
ultimately show \( \text{Exactly_1_of_3_holds} (p, q, r) \) by (rule Fol1_L5 )
A trichotomy law for linear order. This is a special case of strict_ans_tot_trich.
corollary strict_lin_trich:
assumes A1: \( \text{IsLinOrder}(X,r) \) and A2: \( a\in X \), \( b\in X \) and A3: \( s = \text{StrictVersion}(r) \)
shows \( \text{Exactly_1_of_3_holds} (\langle a,b\rangle \in s, a=b,\langle b,a\rangle \in s) \) using assms, IsLinOrder_def, strict_ans_tot_trichFor an antisymmetric relation if a pair is in relation then the reversed pair is not in the strict version of the relation.
lemma geq_impl_not_less:
assumes A1: \( \text{antisym}(r) \) and A2: \( \langle a,b\rangle \in r \)
shows \( \langle b,a\rangle \notin \text{StrictVersion}(r) \)proof{
}
assume A3: \( \langle b,a\rangle \in \text{StrictVersion}(r) \)
with A2 have \( \langle a,b\rangle \in \text{StrictVersion}(r) \) using def_of_strict_ver
with A1, A3 have \( False \) using strict_of_antisym
then show \( \langle b,a\rangle \notin \text{StrictVersion}(r) \)
qed
If an antisymmetric relation is transitive, then the strict version is also transitive, an explicit version strict_of_transB below.
lemma strict_of_transA:
assumes A1: \( \text{trans}(r) \) and A2: \( \text{antisym}(r) \) and A3: \( s= \text{StrictVersion}(r) \) and A4: \( \langle a,b\rangle \in s \), \( \langle b,c\rangle \in s \)
shows \( \langle a,c\rangle \in s \)proof from A3, A4 have I: \( \langle a,b\rangle \in r \wedge \langle b,c\rangle \in r \) using def_of_strict_ver
with A1 have \( \langle a,c\rangle \in r \) by (rule Fol1_L3 )
moreover {
}
qed
assume \( a=c \)
with I have \( \langle a,b\rangle \in r \) and \( \langle b,a\rangle \in r \)
with A2 have \( a=b \) by (rule Fol1_L4 )
with A3, A4 have \( False \) using def_of_strict_ver
then have \( a\neq c \)
ultimately have \( \langle a,c\rangle \in \text{StrictVersion}(r) \) using def_of_strict_ver
with A3 show \( thesis \)
If an antisymmetric relation is transitive, then the strict version is also transitive.
lemma strict_of_transB:
assumes A1: \( \text{trans}(r) \) and A2: \( \text{antisym}(r) \)
shows \( \text{trans}( \text{StrictVersion}(r)) \)proof let \( s = \text{StrictVersion}(r) \)
from A1, A2 have \( \forall x y z.\ \langle x, y\rangle \in s \wedge \langle y, z\rangle \in s \longrightarrow \langle x, z\rangle \in s \) using strict_of_transA
then show \( \text{trans}( \text{StrictVersion}(r)) \) by (rule Fol1_L2 )
qed
The next lemma provides a condition that is satisfied by the strict version of a relation if the original relation is a complete linear order.
lemma strict_of_compl:
assumes A1: \( r \subseteq X\times X \) and A2: \( \text{IsLinOrder}(X,r) \) and A3: \( r \text{ is complete } \) and A4: \( A\subseteq X \), \( A\neq 0 \) and A5: \( s = \text{StrictVersion}(r) \) and A6: \( \exists u\in X.\ \forall y\in A.\ \langle y,u\rangle \in s \)
shows \( \exists x\in X.\ ( \forall y\in A.\ \langle x,y\rangle \notin s ) \wedge (\forall y\in X.\ \langle y,x\rangle \in s \longrightarrow (\exists z\in A.\ \langle y,z\rangle \in s)) \)proof let \( x = \text{Supremum}(r,A) \)
from A2 have I: \( \text{antisym}(r) \) using IsLinOrder_def
moreover
from A5, A6 have \( \exists u\in X.\ \forall y\in A.\ \langle y,u\rangle \in r \) using def_of_strict_ver
moreover note A1, A3, A4
ultimately have II: \( x \in X \), \( \forall y\in A.\ \langle y,x\rangle \in r \) using Order_ZF_5_L7
then have III: \( \exists x\in X.\ \forall y\in A.\ \langle y,x\rangle \in r \)
from A5, I, II have \( x \in X \), \( \forall y\in A.\ \langle x,y\rangle \notin s \) using geq_impl_not_less
moreover
qed
from A1, A2, A3, A4, A5, III have \( \forall y\in X.\ \langle y,x\rangle \in s \longrightarrow (\exists z\in A.\ \langle y,z\rangle \in s) \) using def_of_strict_ver, Order_ZF_5_L8
ultimately show \( \exists x\in X.\ ( \forall y\in A.\ \langle x,y\rangle \notin s ) \wedge (\forall y\in X.\ \langle y,x\rangle \in s \longrightarrow (\exists z\in A.\ \langle y,z\rangle \in s)) \)
Strict version of a relation on a set is a relation on that set.
lemma strict_ver_rel:
assumes A1: \( r \subseteq A\times A \)
shows \( \text{StrictVersion}(r) \subseteq A\times A \) using assms, StrictVersion_def end
Definition of HasAmaximum:
\( \text{HasAmaximum}(r,A) \equiv \exists M\in A.\ \forall x\in A.\ \langle x,M\rangle \in r \)
Definition of HasAminimum:
\( \text{HasAminimum}(r,A) \equiv \exists m\in A.\ \forall x\in A.\ \langle m,x\rangle \in r \)
Definition of HasAsupremum:
\( \text{HasAsupremum}(r,A) \equiv \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)
lemma set_min_not_empty:
assumes \( \text{HasAminimum}(r,A) \)
shows \( A\neq 0 \)Definition of HasAnInfimum:
\( \text{HasAnInfimum}(r,A) \equiv \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)
lemma set_max_not_empty:
assumes \( \text{HasAmaximum}(r,A) \)
shows \( A\neq 0 \) lemma Fol1_L4:
assumes \( \text{antisym}(r) \) and \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \)
shows \( a=b \) lemma Order_ZF_4_L1:
assumes \( \text{antisym}(r) \) and \( \text{HasAmaximum}(r,A) \)
shows \( \exists !M.\ M\in A \wedge (\forall x\in A.\ \langle x,M\rangle \in r) \)Definition of Maximum:
\( \text{Maximum}(r,A) \equiv \text{The } M.\ M\in A \wedge (\forall x\in A.\ \langle x,M\rangle \in r) \)
lemma Order_ZF_4_L2:
assumes \( \text{antisym}(r) \) and \( \text{HasAminimum}(r,A) \)
shows \( \exists !m.\ m\in A \wedge (\forall x\in A.\ \langle m,x\rangle \in r) \)Definition of Minimum:
\( \text{Minimum}(r,A) \equiv \text{The } m.\ m\in A \wedge (\forall x\in A.\ \langle m,x\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 \)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 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_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 \)Definition of SmallerOf:
\( \text{SmallerOf}(r,a,b) \equiv (\text{if }\langle a,b\rangle \in r\text{ then }a\text{ else }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)) \)
lemma Order_ZF_1_L4:
assumes \( r \text{ is total on } X \) and \( A\subseteq X \)
shows \( r \text{ is total on } A \) lemma total_is_refl:
assumes \( r \text{ is total on } X \)
shows \( \text{refl}(X,r) \) lemma Order_ZF_4_L8:
assumes \( \text{refl}(X,r) \) and \( a\in X \)
shows \( \text{HasAmaximum}(r,\{a\}) \), \( \text{HasAminimum}(r,\{a\}) \) lemma Order_ZF_4_L5:
assumes \( r \text{ is total on } (A\cup B) \) and \( \text{trans}(r) \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAmaximum}(r,B) \)
shows \( \text{HasAmaximum}(r,A\cup B) \) lemma Order_ZF_4_L6:
assumes \( r \text{ is total on } (A\cup B) \) and \( \text{trans}(r) \) and \( \text{HasAminimum}(r,A) \), \( \text{HasAminimum}(r,B) \)
shows \( \text{HasAminimum}(r,A\cup B) \) lemma Order_ZF_3_L1B:
assumes \( r \subseteq X\times X \) and \( \text{IsBoundedBelow}(A,r) \)
shows \( A\subseteq X \) lemma Order_ZF_3_L12:
assumes \( \text{IsBoundedBelow}(A,r) \) and \( B\subseteq A \)
shows \( \text{IsBoundedBelow}(B,r) \) lemma Order_ZF_3_L15: shows \( \text{IsBoundedAbove}(\{x\in A.\ \langle x,a\rangle \in r\},r) \)
Definition of IsBounded:
\( \text{IsBounded}(A,r) \equiv ( \text{IsBoundedAbove}(A,r) \wedge \text{IsBoundedBelow}(A,r)) \)
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\} \) 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_3_L1A:
assumes \( r \subseteq X\times X \) and \( \text{IsBoundedAbove}(A,r) \)
shows \( A\subseteq X \) lemma Order_ZF_3_L13:
assumes \( \text{IsBoundedAbove}(A,r) \) and \( B\subseteq A \)
shows \( \text{IsBoundedAbove}(B,r) \) lemma Order_ZF_4_L4:
assumes \( \text{antisym}(r) \) and \( \text{HasAminimum}(r,A) \)
shows \( \text{Minimum}(r,A) \in A \), \( \forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r \) lemma Order_ZF_4_L3:
assumes \( \text{antisym}(r) \) and \( \text{HasAmaximum}(r,A) \)
shows \( \text{Maximum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,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 Supremum:
\( \text{Supremum}(r,A) \equiv \text{Minimum}(r,\bigcap a\in A.\ r\{a\}) \)
lemma set_sup_not_empty:
assumes \( \text{HasAsupremum}(r,A) \)
shows \( A\neq 0 \)Definition of Infimum:
\( \text{Infimum}(r,A) \equiv \text{Maximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)
lemma set_inf_not_empty:
assumes \( \text{HasAnInfimum}(r,A) \)
shows \( A\neq 0 \) lemma Order_ZF_4_L15:
assumes \( \text{antisym}(r) \) and \( m \in A \) and \( \forall a\in A.\ \langle m,a\rangle \in r \)
shows \( \text{Minimum}(r,A) = m \) lemma Order_ZF_4_L14:
assumes \( \text{antisym}(r) \) and \( M \in A \) and \( \forall a\in A.\ \langle a,M\rangle \in r \)
shows \( \text{Maximum}(r,A) = M \) lemma inf_glb:
assumes \( \text{antisym}(r) \), \( A\neq 0 \), \( \forall x\in A.\ \langle z,x\rangle \in r \), \( \forall y.\ (\forall x\in A.\ \langle y,x\rangle \in r) \longrightarrow \langle y,z\rangle \in r \)
shows \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \), \( z = \text{Infimum}(r,A) \) lemma Order_ZF_5_L5:
assumes \( \text{antisym}(r) \) and \( A\neq 0 \) and \( \forall x\in A.\ \langle x,z\rangle \in r \) and \( \forall y.\ (\forall x\in A.\ \langle x,y\rangle \in r) \longrightarrow \langle z,y\rangle \in r \)
shows \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \), \( z = \text{Supremum}(r,A) \) lemma Order_ZF_5_L5:
assumes \( \text{antisym}(r) \) and \( A\neq 0 \) and \( \forall x\in A.\ \langle x,z\rangle \in r \) and \( \forall y.\ (\forall x\in A.\ \langle x,y\rangle \in r) \longrightarrow \langle z,y\rangle \in r \)
shows \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \), \( z = \text{Supremum}(r,A) \) lemma Order_ZF_5_L5:
assumes \( \text{antisym}(r) \) and \( A\neq 0 \) and \( \forall x\in A.\ \langle x,z\rangle \in r \) and \( \forall y.\ (\forall x\in A.\ \langle x,y\rangle \in r) \longrightarrow \langle z,y\rangle \in r \)
shows \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \), \( z = \text{Supremum}(r,A) \) lemma inf_glb:
assumes \( \text{antisym}(r) \), \( A\neq 0 \), \( \forall x\in A.\ \langle z,x\rangle \in r \), \( \forall y.\ (\forall x\in A.\ \langle y,x\rangle \in r) \longrightarrow \langle y,z\rangle \in r \)
shows \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \), \( z = \text{Infimum}(r,A) \) lemma inf_glb:
assumes \( \text{antisym}(r) \), \( A\neq 0 \), \( \forall x\in A.\ \langle z,x\rangle \in r \), \( \forall y.\ (\forall x\in A.\ \langle y,x\rangle \in r) \longrightarrow \langle y,z\rangle \in r \)
shows \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \), \( z = \text{Infimum}(r,A) \) lemma min_max_two_el:
assumes \( r \text{ is total on } X \), \( x\in X \), \( y\in X \)
shows \( \text{HasAminimum}(r,\{x,y\}) \) and \( \text{HasAmaximum}(r,\{x,y\}) \) lemma max_is_sup:
assumes \( \text{antisym}(r) \), \( A\neq 0 \), \( \text{HasAmaximum}(r,A) \)
shows \( \text{HasAsupremum}(r,A) \) and \( \text{Maximum}(r,A) = \text{Supremum}(r,A) \) lemma min_is_inf:
assumes \( \text{antisym}(r) \), \( A\neq 0 \), \( \text{HasAminimum}(r,A) \)
shows \( \text{HasAnInfimum}(r,A) \) and \( \text{Minimum}(r,A) = \text{Infimum}(r,A) \) lemma Order_ZF_5_L1:
assumes \( u \in (\bigcap a\in A.\ r\{a\}) \) and \( a\in A \)
shows \( \langle a,u\rangle \in r \)Definition of IsComplete:
\( 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\}) \)
lemma sup_in_space:
assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)
shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \) lemma inf_in_space:
assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAmaximum}(r,\bigcap a\in A.\ r^{-1}\{a\}) \)
shows \( \text{Infimum}(r,A) \in X \) and \( \forall x\in A.\ \langle \text{Infimum}(r,A),x\rangle \in r \) lemma inf_geq_lo_bnd:
assumes \( \text{antisym}(r) \), \( \text{HasAnInfimum}(r,A) \), \( \forall a\in A.\ \langle u,a\rangle \in r \)
shows \( \langle u, \text{Infimum}(r,A)\rangle \in r \) lemma sup_in_space:
assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \)
shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \) lemma sup_leq_up_bnd:
assumes \( \text{antisym}(r) \), \( \text{HasAsupremum}(r,A) \), \( \forall a\in A.\ \langle a,u\rangle \in r \)
shows \( \langle \text{Supremum}(r,A),u\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) \)
lemma Order_ZF_5_L3:
assumes \( \text{antisym}(r) \) and \( A\neq 0 \) and \( \text{HasAminimum}(r,\bigcap a\in A.\ r\{a\}) \) and \( \forall a\in A.\ \langle a,u\rangle \in r \)
shows \( \langle \text{Supremum}(r,A),u\rangle \in r \)Definition of StrictVersion:
\( \text{StrictVersion}(r) \equiv r - \{\langle x,x\rangle .\ x \in domain(r)\} \)
lemma def_of_strict_ver: shows \( \langle x,y\rangle \in \text{StrictVersion}(r) \longleftrightarrow \langle x,y\rangle \in r \wedge x\neq y \)
lemma strict_of_tot:
assumes \( r \text{ is total on } X \) and \( a\in X \), \( b\in X \), \( a\neq b \)
shows \( \langle a,b\rangle \in \text{StrictVersion}(r) \vee \langle b,a\rangle \in \text{StrictVersion}(r) \) lemma strict_of_antisym:
assumes \( \text{antisym}(r) \) and \( \langle a,b\rangle \in \text{StrictVersion}(r) \)
shows \( \langle b,a\rangle \notin \text{StrictVersion}(r) \) lemma Fol1_L5:
assumes \( p\vee q\vee r \) and \( p \longrightarrow \neg q \wedge \neg r \) and \( q \longrightarrow \neg p \wedge \neg r \) and \( r \longrightarrow \neg p \wedge \neg q \)
shows \( \text{Exactly_1_of_3_holds} (p,q,r) \) lemma strict_ans_tot_trich:
assumes \( \text{antisym}(r) \) and \( r \text{ is total on } X \) and \( a\in X \), \( b\in X \) and \( s = \text{StrictVersion}(r) \)
shows \( \text{Exactly_1_of_3_holds} (\langle a,b\rangle \in s, a=b,\langle b,a\rangle \in s) \) lemma strict_of_transA:
assumes \( \text{trans}(r) \) and \( \text{antisym}(r) \) and \( s= \text{StrictVersion}(r) \) and \( \langle a,b\rangle \in s \), \( \langle b,c\rangle \in s \)
shows \( \langle a,c\rangle \in s \) lemma Fol1_L2:
assumes \( \forall x y z.\ \langle x, y\rangle \in r \wedge \langle y, z\rangle \in r \longrightarrow \langle x, z\rangle \in r \)
shows \( \text{trans}(r) \) lemma Order_ZF_5_L7:
assumes \( r \subseteq X\times X \) and \( \text{antisym}(r) \) and \( r \text{ is complete } \) and \( A\neq 0 \) and \( \exists x\in X.\ \forall y\in A.\ \langle y,x\rangle \in r \)
shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \) lemma geq_impl_not_less:
assumes \( \text{antisym}(r) \) and \( \langle a,b\rangle \in r \)
shows \( \langle b,a\rangle \notin \text{StrictVersion}(r) \) lemma Order_ZF_5_L8:
assumes \( r \subseteq X\times X \) and \( \text{IsLinOrder}(X,r) \) and \( r \text{ is complete } \) and \( A\subseteq X \), \( A\neq 0 \) and \( \exists x\in X.\ \forall y\in A.\ \langle y,x\rangle \in r \) and \( \langle y, \text{Supremum}(r,A)\rangle \in r \), \( y \neq \text{Supremum}(r,A) \)
shows \( \exists z\in A.\ \langle y,z\rangle \in r \wedge y \neq z \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8