begin
In this theory we consider some properties of functions related to order relations
Functions and order
This section deals with functions between ordered sets.
If every value of a function on a set is bounded below by a constant, then the image of the set is bounded below.
lemma func_ZF_8_L1:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall x\in A.\ \langle L,f(x)\rangle \in r \)
shows \( \text{IsBoundedBelow}(f(A),r) \)proof from assms have \( \forall y \in f(A).\ \langle L,y\rangle \in r \) using func_imagedef
then show \( \text{IsBoundedBelow}(f(A),r) \) by (rule Order_ZF_3_L9 )
qed
If every value of a function on a set is bounded above by a constant, then the image of the set is bounded above.
lemma func_ZF_8_L2:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall x\in A.\ \langle f(x),U\rangle \in r \)
shows \( \text{IsBoundedAbove}(f(A),r) \)proof from assms have \( \forall y \in f(A).\ \langle y,U\rangle \in r \) using func_imagedef
then show \( \text{IsBoundedAbove}(f(A),r) \) by (rule Order_ZF_3_L10 )
qed
Identity is an order isomorphism.
lemma id_ord_iso:
shows \( id(X) \in ord\_iso(X,r,X,r) \) using id_bij, id_def, ord_iso_defIdentity is the only order automorphism of a singleton.
lemma id_ord_auto_singleton:
shows \( ord\_iso(\{x\},r,\{x\},r) = \{id(\{x\})\} \) using id_ord_iso, ord_iso_def, single_bij_idThe image of a maximum by an order isomorphism is a maximum. Note that from the fact the \(r\) is antisymmetric and \(f\) is an order isomorphism between \((A,r)\) and \((B,R)\) we can not conclude that \(R\) is antisymmetric (we can only show that \(R\cap (B\times B)\) is).
lemma max_image_ord_iso:
assumes A1: \( \text{antisym}(r) \) and A2: \( \text{antisym}(R) \) and A3: \( f \in ord\_iso(A,r,B,R) \) and A4: \( \text{HasAmaximum}(r,A) \)
shows \( \text{HasAmaximum}(R,B) \) and \( \text{Maximum}(R,B) = f( \text{Maximum}(r,A)) \)proof let \( M = \text{Maximum}(r,A) \)
from A1, A4 have \( M \in A \) using Order_ZF_4_L3
from A3 have \( f:A\rightarrow B \) using ord_iso_def, bij_is_fun
with \( M \in A \) have I: \( f(M) \in B \) using apply_funtype
{
fix \( y \)
assume \( y \in B \)
let \( x = converse(f)(y) \)
from A3 have \( converse(f) \in ord\_iso(B,R,A,r) \) using ord_iso_sym
then have \( converse(f): B \rightarrow A \) using ord_iso_def, bij_is_fun
with \( y \in B \) have \( x \in A \)
with A1, A3, A4, \( x \in A \), \( M \in A \) have \( \langle f(x), f(M)\rangle \in R \) using Order_ZF_4_L3, ord_iso_apply
with A3, \( y \in B \) have \( \langle y, f(M)\rangle \in R \) using right_inverse_bij, ord_iso_def
then have II: \( \forall y \in B.\ \langle y, f(M)\rangle \in R \)
with A2, I show \( \text{Maximum}(R,B) = f(M) \) by (rule Order_ZF_4_L14 )
from I, II show \( \text{HasAmaximum}(R,B) \) using HasAmaximum_def
qed
Maximum is a fixpoint of order automorphism.
lemma max_auto_fixpoint:
assumes \( \text{antisym}(r) \) and \( f \in ord\_iso(A,r,A,r) \) and \( \text{HasAmaximum}(r,A) \)
shows \( \text{Maximum}(r,A) = f( \text{Maximum}(r,A)) \) using assms, max_image_ord_isoIf two sets are order isomorphic and we remove \(x\) and \(f(x)\), respectively, from the sets, then they are still order isomorphic.
lemma ord_iso_rem_point:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( a \in A \)
shows \( \text{restrict}(f,A-\{a\}) \in ord\_iso(A-\{a\},r,B-\{f(a)\},R) \)proof let \( f_0 = \text{restrict}(f,A-\{a\}) \)
have \( A-\{a\} \subseteq A \)
with A1 have \( f_0 \in ord\_iso(A-\{a\},r,f(A-\{a\}),R) \) using ord_iso_restrict_image
moreover
qed
from A1 have \( f \in \text{inj}(A,B) \) using ord_iso_def, bij_def
with A2 have \( f(A-\{a\}) = f(A) - f\{a\} \) using inj_image_dif
moreover from A1 have \( f(A) = B \) using ord_iso_def, bij_def, surj_range_image_domain
moreover from A1 have \( f: A\rightarrow B \) using ord_iso_def, bij_is_fun
with A2 have \( f\{a\} = \{f(a)\} \) using singleton_image
ultimately show \( thesis \)
If two sets are order isomorphic and we remove maxima from the sets, then they are still order isomorphic.
corollary ord_iso_rem_max:
assumes A1: \( \text{antisym}(r) \) and \( f \in ord\_iso(A,r,B,R) \) and A4: \( \text{HasAmaximum}(r,A) \) and A5: \( M = \text{Maximum}(r,A) \)
shows \( \text{restrict}(f,A-\{M\}) \in ord\_iso(A-\{M\}, r, B-\{f(M)\},R) \) using assms, Order_ZF_4_L3, ord_iso_rem_pointLemma about extending order isomorphisms by adding one point to the domain.
lemma ord_iso_extend:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( M_A \notin A \), \( M_B \notin B \) and A3: \( \forall a\in A.\ \langle a, M_A\rangle \in r \), \( \forall b\in B.\ \langle b, M_B\rangle \in R \) and A4: \( \text{antisym}(r) \), \( \text{antisym}(R) \) and A5: \( \langle M_A,M_A\rangle \in r \longleftrightarrow \langle M_B,M_B\rangle \in R \)
shows \( f \cup \{\langle M_A,M_B\rangle \} \in ord\_iso(A\cup \{M_A\} ,r,B\cup \{M_B\} ,R) \)proof let \( g = f \cup \{\langle M_A,M_B\rangle \} \)
from A1, A2 have \( g : A\cup \{M_A\} \rightarrow B\cup \{M_B\} \) and I: \( \forall x\in A.\ g(x) = f(x) \) and II: \( g(M_A) = M_B \) using ord_iso_def, bij_def, inj_def, func1_1_L11D
from A1, A2 have \( g \in \text{bij}(A\cup \{M_A\},B\cup \{M_B\}) \) using ord_iso_def, bij_extend_point
moreover
qed
have \( \forall x \in A\cup \{M_A\}.\ \forall y \in A\cup \{M_A\}.\ \)
\( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \)proof
ultimately show \( thesis \) using ord_iso_def
{
}
fix \( x \) \( y \)
assume \( x \in A\cup \{M_A\} \) and \( y \in A\cup \{M_A\} \)
then have \( x\in A \wedge y \in A \vee x\in A \wedge y = M_A \vee \)
\( x = M_A \wedge y \in A \vee x = M_A \wedge y = M_A \)
moreover {
}
moreover {
}
moreover {
}
moreover {
}
ultimately have \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \)
assume \( x\in A \wedge y \in A \)
with A1, I have \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \) using ord_iso_def
assume \( x\in A \wedge y = M_A \)
with A1, A3, I, II have \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \) using ord_iso_def, bij_def, inj_def, apply_funtype
assume \( x = M_A \wedge y \in A \)
with A2, A3, A4 have \( \langle x,y\rangle \notin r \) using antisym_def
moreover {
}
assume A6: \( \langle g(x), g(y)\rangle \in R \)
from A1, I, II, \( x = M_A \wedge y \in A \) have III: \( g(y) \in B \), \( g(x) = M_B \) using ord_iso_def, bij_def, inj_def, apply_funtype
with A3 have \( \langle g(y), g(x)\rangle \in R \)
with A4, A6 have \( g(y) = g(x) \) using antisym_def
with A2, III have \( False \)
hence \( \langle g(x), g(y)\rangle \notin R \)
ultimately have \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \)
assume \( x = M_A \wedge y = M_A \)
with A5, II have \( \langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R \)
thus \( thesis \)
qed
A kind of converse to ord_iso_rem_max: if two linearly ordered sets sets are order isomorphic after removing the maxima, then they are order isomorphic.
lemma rem_max_ord_iso:
assumes A1: \( \text{IsLinOrder}(X,r) \), \( \text{IsLinOrder}(Y,R) \) and A2: \( \text{HasAmaximum}(r,X) \), \( \text{HasAmaximum}(R,Y) \), \( ord\_iso(X - \{ \text{Maximum}(r,X)\},r,Y - \{ \text{Maximum}(R,Y)\},R) \neq 0 \)
shows \( ord\_iso(X,r,Y,R) \neq 0 \)proof let \( M_A = \text{Maximum}(r,X) \)
let \( A = X - \{M_A\} \)
let \( M_B = \text{Maximum}(R,Y) \)
let \( B = Y - \{M_B\} \)
from A2 obtain \( f \) where \( f \in ord\_iso(A,r,B,R) \)
moreover
have \( M_A \notin A \) and \( M_B \notin B \)
moreover from A1, A2 have \( \forall a\in A.\ \langle a,M_A\rangle \in r \) and \( \forall b\in B.\ \langle b,M_B\rangle \in R \) using IsLinOrder_def, Order_ZF_4_L3
moreover from A1 have \( \text{antisym}(r) \) and \( \text{antisym}(R) \) using IsLinOrder_def
moreover from A1, A2 have \( \langle M_A,M_A\rangle \in r \longleftrightarrow \langle M_B,M_B\rangle \in R \) using IsLinOrder_def, Order_ZF_4_L3, IsLinOrder_def, total_is_refl, refl_def
ultimately have \( f \cup \{\langle M_A,M_B\rangle \} \in ord\_iso(A\cup \{M_A\} ,r,B\cup \{M_B\} ,R) \) by (rule ord_iso_extend )
moreover
qed
from A1, A2 have \( A\cup \{M_A\} = X \) and \( B\cup \{M_B\} = Y \) using IsLinOrder_def, Order_ZF_4_L3
ultimately show \( ord\_iso(X,r,Y,R) \neq 0 \) using ord_iso_extend
Functions in cartesian products
In this section we consider maps arising naturally in cartesian products.
There is a natural bijection etween \(X=Y\times \{ y\}\) (a "slice") and \(Y\). We will call this the \( \text{SliceProjection}(Y\times \{y\}) \). This is really the ZF equivalent of the meta-function \( \text{fst}(x) \).
definition
\( \text{SliceProjection}(X) \equiv \{\langle p,\text{fst}(p)\rangle .\ p \in X \} \)
A slice projection is a bijection between \(X\times\{ y\}\) and \(X\).
lemma slice_proj_bij:
shows \( \text{SliceProjection}(X\times \{y\}): X\times \{y\} \rightarrow X \), \( domain( \text{SliceProjection}(X\times \{y\})) = X\times \{y\} \), \( \forall p\in X\times \{y\}.\ \text{SliceProjection}(X\times \{y\})(p) = \text{fst}(p) \), \( \text{SliceProjection}(X\times \{y\}) \in \text{bij}(X\times \{y\},X) \)proof let \( P = \text{SliceProjection}(X\times \{y\}) \)
have \( \forall p \in X\times \{y\}.\ \text{fst}(p) \in X \)
moreover
from this have \( \{\langle p,\text{fst}(p)\rangle .\ p \in X\times \{y\} \} : X\times \{y\} \rightarrow X \) by (rule ZF_fun_from_total )
ultimately show I: \( P: X\times \{y\} \rightarrow X \) and II: \( \forall p\in X\times \{y\}.\ P(p) = \text{fst}(p) \) using ZF_fun_from_tot_val, SliceProjection_def
hence \( \forall a \in X\times \{y\}.\ \forall b \in X\times \{y\}.\ P(a) = P(b) \longrightarrow a=b \)
with I have \( P \in \text{inj}(X\times \{y\},X) \) using inj_def
moreover
from II have \( \forall x\in X.\ \exists p\in X\times \{y\}.\ P(p) = x \)
with I have \( P \in \text{surj}(X\times \{y\},X) \) using surj_def
ultimately show \( P \in \text{bij}(X\times \{y\},X) \) using bij_def
from I show \( domain( \text{SliceProjection}(X\times \{y\})) = X\times \{y\} \) using func1_1_L1
qed
Given 2 functions \(f:A\to B\) and \(g:C\to D\) , we can consider a function \(h:A\times C \to B\times D\) such that \(h(x,y)=\langle f(x),g(y)\rangle\)
definition
\( \text{ProdFunction}(f,g) \equiv \{\langle z,\langle f(\text{fst}(z)),g(\text{snd}(z))\rangle \rangle .\ z\in domain(f)\times domain(g)\} \)
For given functions \(f:A\to B\) and \(g:C\to D\) the function \( \text{ProdFunction}(f,g) \) maps \(A\times C\) to \(B\times D\).
lemma prodFunction:
assumes \( f:A\rightarrow B \), \( g:C\rightarrow D \)
shows \( \text{ProdFunction}(f,g):(A\times C)\rightarrow (B\times D) \)proof from assms have \( \forall z \in domain(f)\times domain(g).\ \langle f(\text{fst}(z)),g(\text{snd}(z))\rangle \in B\times D \) using func1_1_L1, apply_type
with assms show \( thesis \) unfolding ProdFunction_def using func1_1_L1, ZF_fun_from_total
qed
For given functions \(f:A\to B\) and \(g:C\to D\) and points \(x\in A\), \(y\in C\) the value of the function \( \text{ProdFunction}(f,g) \) on \(\langle x,y \rangle\) is \(\langle f(x),g(y) \rangle\).
lemma prodFunctionApp:
assumes \( f:A\rightarrow B \), \( g:C\rightarrow D \), \( x\in A \), \( y\in C \)
shows \( \text{ProdFunction}(f,g)\langle x,y\rangle = \langle f(x),g(y)\rangle \)proof let \( z = \langle x,y\rangle \)
from assms have \( z \in A\times C \) and \( \text{ProdFunction}(f,g):(A\times C)\rightarrow (B\times D) \) using prodFunction
moreover
qed
from assms(1,2) have \( \text{ProdFunction}(f,g) = \{\langle z,\langle f(\text{fst}(z)),g(\text{snd}(z))\rangle \rangle .\ z\in A\times C\} \) unfolding ProdFunction_def using func1_1_L1
ultimately show \( thesis \) using ZF_fun_from_tot_val
Somewhat technical lemma about inverse image of a set by a \( \text{ProdFunction}(f,f) \).
lemma prodFunVimage:
assumes \( x\in X \), \( f:X\rightarrow Y \)
shows \( \langle x,t\rangle \in \text{ProdFunction}(f,f)^{-1}(V) \longleftrightarrow t\in X \wedge \langle fx,ft\rangle \in V \)proof from assms(2) have T: \( \text{ProdFunction}(f,f)^{-1}(V) = \{z \in X\times X.\ \text{ProdFunction}(f,f)(z) \in V\} \) using prodFunction, func1_1_L15
with assms show \( thesis \) using prodFunctionApp
qed
Induced relations and order isomorphisms
When we have two sets \(X,Y\), function \(f:X\rightarrow Y\) and a relation \(R\) on \(Y\) we can define a relation \(r\) on \(X\) by saying that \(x\ r\ y\) if and only if \(f(x) \ R \ f(y)\). This is especially interesting when \(f\) is a bijection as all reasonable properties of \(R\) are inherited by \(r\). This section treats mostly the case when \(R\) is an order relation and \(f\) is a bijection. The standard Isabelle's Order theory defines the notion of a space of order isomorphisms between two sets relative to a relation. We expand that material proving that order isomrphisms preserve interesting properties of the relation.
We call the relation created by a relation on \(Y\) and a mapping \(f:X\rightarrow Y\) the \( \text{InducedRelation}(f,R) \).
definition
\( \text{InducedRelation}(f,R) \equiv \) \( \{p \in domain(f)\times domain(f).\ \langle f(\text{fst}(p)),f(\text{snd}(p))\rangle \in R\} \)
A reformulation of the definition of the relation induced by a function.
lemma def_of_ind_relA:
assumes \( \langle x,y\rangle \in \text{InducedRelation}(f,R) \)
shows \( \langle f(x),f(y)\rangle \in R \) using assms, InducedRelation_defA reformulation of the definition of the relation induced by a function, kind of converse of def_of_ind_relA.
lemma def_of_ind_relB:
assumes \( f:A\rightarrow B \) and \( x\in A \), \( y\in A \) and \( \langle f(x),f(y)\rangle \in R \)
shows \( \langle x,y\rangle \in \text{InducedRelation}(f,R) \) using assms, func1_1_L1, InducedRelation_defA property of order isomorphisms that is missing from standard Isabelle's Order.thy.
lemma ord_iso_apply_conv:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( \langle f(x),f(y)\rangle \in R \) and \( x\in A \), \( y\in A \)
shows \( \langle x,y\rangle \in r \) using assms, ord_iso_defThe next lemma tells us where the induced relation is defined
lemma ind_rel_domain:
assumes \( R \subseteq B\times B \) and \( f:A\rightarrow B \)
shows \( \text{InducedRelation}(f,R) \subseteq A\times A \) using assms, func1_1_L1, InducedRelation_defA bijection is an order homomorphisms between a relation and the induced one.
lemma bij_is_ord_iso:
assumes A1: \( f \in \text{bij}(A,B) \)
shows \( f \in ord\_iso(A, \text{InducedRelation}(f,R),B,R) \)proof let \( r = \text{InducedRelation}(f,R) \)
{
fix \( x \) \( y \)
assume A2: \( x\in A \), \( y\in A \)
have \( \langle x,y\rangle \in r \longleftrightarrow \langle f(x),f(y)\rangle \in R \)proof
assume \( \langle x,y\rangle \in r \)
then show \( \langle f(x),f(y)\rangle \in R \) using def_of_ind_relA
next
assume \( \langle f(x),f(y)\rangle \in R \)
with A1, A2 show \( \langle x,y\rangle \in r \) using bij_is_fun, def_of_ind_relB
qed
with A1 show \( f \in ord\_iso(A, \text{InducedRelation}(f,R),B,R) \) using ord_isoI
qed
An order isomoprhism preserves antisymmetry.
lemma ord_iso_pres_antsym:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \) and A3: \( \text{antisym}(R) \)
shows \( \text{antisym}(r) \)proof{
}
fix \( x \) \( y \)
assume A4: \( \langle x,y\rangle \in r \), \( \langle y,x\rangle \in r \)
from A1 have \( f \in \text{inj}(A,B) \) using ord_iso_is_bij, bij_is_inj
moreover
from A1, A2, A4 have \( \langle f(x), f(y)\rangle \in R \) and \( \langle f(y), f(x)\rangle \in R \) using ord_iso_apply
with A3 have \( f(x) = f(y) \) by (rule Fol1_L4 )
moreover from A2, A4 have \( x\in A \), \( y\in A \)
ultimately have \( x=y \) by (rule inj_apply_equality )
then have \( \forall x y.\ \langle x,y\rangle \in r \wedge \langle y,x\rangle \in r \longrightarrow x=y \)
then show \( \text{antisym}(r) \) using imp_conj, antisym_def
qed
Order isomoprhisms preserve transitivity.
lemma ord_iso_pres_trans:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \) and A3: \( \text{trans}(R) \)
shows \( \text{trans}(r) \)proof{
}
fix \( x \) \( y \) \( z \)
assume A4: \( \langle x, y\rangle \in r \), \( \langle y, z\rangle \in r \)
note A1
moreover
from A1, A2, A4 have \( \langle f(x), f(y)\rangle \in R \wedge \langle f(y), f(z)\rangle \in R \) using ord_iso_apply
with A3 have \( \langle f(x),f(z)\rangle \in R \) by (rule Fol1_L3 )
moreover from A2, A4 have \( x\in A \), \( z\in A \)
ultimately have \( \langle x, z\rangle \in r \) using ord_iso_apply_conv
then have \( \forall x y z.\ \langle x, y\rangle \in r \wedge \langle y, z\rangle \in r \longrightarrow \langle x, z\rangle \in r \)
then show \( \text{trans}(r) \) by (rule Fol1_L2 )
qed
Order isomorphisms preserve totality.
lemma ord_iso_pres_tot:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \) and A3: \( R \text{ is total on } B \)
shows \( r \text{ is total on } A \)proof{
}
fix \( x \) \( y \)
assume \( x\in A \), \( y\in A \), \( \langle x,y\rangle \notin r \)
with A1 have \( \langle f(x),f(y)\rangle \notin R \) using ord_iso_apply_conv
moreover
from A1 have \( f:A\rightarrow B \) using ord_iso_is_bij, bij_is_fun
with A3, \( x\in A \), \( y\in A \) have \( \langle f(x),f(y)\rangle \in R \vee \langle f(y),f(x)\rangle \in R \) using apply_funtype, IsTotal_def
ultimately have \( \langle f(y),f(x)\rangle \in R \)
with A1, \( x\in A \), \( y\in A \) have \( \langle y,x\rangle \in r \) using ord_iso_apply_conv
then have \( \forall x\in A.\ \forall y\in A.\ \langle x,y\rangle \in r \vee \langle y,x\rangle \in r \)
then show \( r \text{ is total on } A \) using IsTotal_def
qed
Order isomorphisms preserve linearity.
lemma ord_iso_pres_lin:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{IsLinOrder}(B,R) \)
shows \( \text{IsLinOrder}(A,r) \) using assms, ord_iso_pres_antsym, ord_iso_pres_trans, ord_iso_pres_tot, IsLinOrder_defIf a relation is a linear order, then the relation induced on another set by a bijection is also a linear order.
lemma ind_rel_pres_lin:
assumes A1: \( f \in \text{bij}(A,B) \) and A2: \( \text{IsLinOrder}(B,R) \)
shows \( \text{IsLinOrder}(A, \text{InducedRelation}(f,R)) \)proof let \( r = \text{InducedRelation}(f,R) \)
from A1 have \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) using bij_is_ord_iso, domain_of_bij, InducedRelation_def
with A2 show \( \text{IsLinOrder}(A,r) \) using ord_iso_pres_lin
qed
The image by an order isomorphism of a bounded above and nonempty set is bounded above.
lemma ord_iso_pres_bound_above:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \) and A3: \( \text{IsBoundedAbove}(C,r) \), \( C\neq 0 \)
shows \( \text{IsBoundedAbove}(f(C),R) \), \( f(C) \neq 0 \)proof from A3 obtain \( u \) where I: \( \forall x\in C.\ \langle x,u\rangle \in r \) using IsBoundedAbove_def
from A1 have \( f:A\rightarrow B \) using ord_iso_is_bij, bij_is_fun
from A2, A3 have \( C\subseteq A \) using Order_ZF_3_L1A
from A3 obtain \( x \) where \( x\in C \)
with A2, I have \( u\in A \)
{
fix \( y \)
assume \( y \in f(C) \)
with \( f:A\rightarrow B \), \( C\subseteq A \) obtain \( x \) where \( x\in C \) and \( y = f(x) \) using func_imagedef
with A1, I, \( C\subseteq A \), \( u\in A \) have \( \langle y,f(u)\rangle \in R \) using ord_iso_apply
then have \( \forall y \in f(C).\ \langle y,f(u)\rangle \in R \)
then show \( \text{IsBoundedAbove}(f(C),R) \) by (rule Order_ZF_3_L10 )
from A3, \( f:A\rightarrow B \), \( C\subseteq A \) show \( f(C) \neq 0 \) using func1_1_L15A
qed
Order isomorphisms preserve the property of having a minimum.
lemma ord_iso_pres_has_min:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \) and A3: \( C\subseteq A \) and A4: \( \text{HasAminimum}(R,f(C)) \)
shows \( \text{HasAminimum}(r,C) \)proof from A4 obtain \( m \) where I: \( m \in f(C) \) and II: \( \forall y \in f(C).\ \langle m,y\rangle \in R \) using HasAminimum_def
let \( k = converse(f)(m) \)
from A1 have \( f:A\rightarrow B \) using ord_iso_is_bij, bij_is_fun
from A1 have \( f \in \text{inj}(A,B) \) using ord_iso_is_bij, bij_is_inj
with A3, I have \( k \in C \) and III: \( f(k) = m \) using inj_inv_back_in_set
moreover {
}
qed
fix \( x \)
assume A5: \( x\in C \)
with A3, II, \( f:A\rightarrow B \), \( k \in C \), III have \( k \in A \), \( x\in A \), \( \langle f(k),f(x)\rangle \in R \) using func_imagedef
with A1 have \( \langle k,x\rangle \in r \) using ord_iso_apply_conv
then have \( \forall x\in C.\ \langle k,x\rangle \in r \)
ultimately show \( \text{HasAminimum}(r,C) \) using HasAminimum_def
Order isomorhisms preserve the images of relations. In other words taking the image of a point by a relation commutes with the function.
lemma ord_iso_pres_rel_image:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \), \( R \subseteq B\times B \) and A3: \( a\in A \)
shows \( f(r\{a\}) = R\{f(a)\} \)proof from A1 have \( f:A\rightarrow B \) using ord_iso_is_bij, bij_is_fun
moreover
{
from A2, A3 have I: \( r\{a\} \subseteq A \)
ultimately have I: \( f(r\{a\}) = \{f(x).\ x \in r\{a\} \} \) using func_imagedef
fix \( y \)
assume A4: \( y \in f(r\{a\}) \)
with I obtain \( x \) where \( x \in r\{a\} \) and II: \( y = f(x) \)
with A1, A2 have \( \langle f(a),f(x)\rangle \in R \) using ord_iso_apply
with II have \( y \in R\{f(a)\} \)
then show \( f(r\{a\}) \subseteq R\{f(a)\} \)
{
fix \( y \)
assume A5: \( y \in R\{f(a)\} \)
let \( x = converse(f)(y) \)
from A2, A5 have \( \langle f(a),y\rangle \in R \), \( f(a) \in B \) and IV: \( y\in B \)
with A1 have III: \( \langle converse(f)(f(a)),x\rangle \in r \) using ord_iso_converse
moreover
from A1, A3 have \( converse(f)(f(a)) = a \) using ord_iso_is_bij, left_inverse_bij
ultimately have \( f(x) \in \{f(x).\ x \in r\{a\} \} \)
moreover
from A1, IV have \( f(x) = y \) using ord_iso_is_bij, right_inverse_bij
moreover from A1, I have \( f(r\{a\}) = \{f(x).\ x \in r\{a\} \} \) using ord_iso_is_bij, bij_is_fun, func_imagedef
ultimately have \( y \in f(r\{a\}) \)
then show \( R\{f(a)\} \subseteq f(r\{a\}) \)
qed
Order isomorphisms preserve collections of upper bounds.
lemma ord_iso_pres_up_bounds:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \), \( R \subseteq B\times B \) and A3: \( C\subseteq A \)
shows \( \{f(r\{a\}).\ a\in C\} = \{R\{b\}.\ b \in f(C)\} \)proof from A1 have \( f:A\rightarrow B \) using ord_iso_is_bij, bij_is_fun
{
fix \( Y \)
assume \( Y \in \{f(r\{a\}).\ a\in C\} \)
then obtain \( a \) where \( a\in C \) and I: \( Y = f(r\{a\}) \)
from A3, \( a\in C \) have \( a\in A \)
with A1, A2 have \( f(r\{a\}) = R\{f(a)\} \) using ord_iso_pres_rel_image
moreover
from A3, \( f:A\rightarrow B \), \( a\in C \) have \( f(a) \in f(C) \) using func_imagedef
ultimately have \( f(r\{a\}) \in \{ R\{b\}.\ b \in f(C) \} \)
with I have \( Y \in \{ R\{b\}.\ b \in f(C) \} \)
then show \( \{f(r\{a\}).\ a\in C\} \subseteq \{R\{b\}.\ b \in f(C)\} \)
{
fix \( Y \)
assume \( Y \in \{R\{b\}.\ b \in f(C)\} \)
then obtain \( b \) where \( b \in f(C) \) and II: \( Y = R\{b\} \)
with A3, \( f:A\rightarrow B \) obtain \( a \) where \( a\in C \) and \( b = f(a) \) using func_imagedef
with A3, II have \( a\in A \) and \( Y = R\{f(a)\} \)
with A1, A2 have \( Y = f(r\{a\}) \) using ord_iso_pres_rel_image
with \( a\in C \) have \( Y \in \{f(r\{a\}).\ a\in C\} \)
then show \( \{R\{b\}.\ b \in f(C)\} \subseteq \{f(r\{a\}).\ a\in C\} \)
qed
The image of the set of upper bounds is the set of upper bounds of the image.
lemma ord_iso_pres_min_up_bounds:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \), \( R \subseteq B\times B \) and A3: \( C\subseteq A \) and A4: \( C\neq 0 \)
shows \( f(\bigcap a\in C.\ r\{a\}) = (\bigcap b\in f(C).\ R\{b\}) \)proof from A1 have \( f \in \text{inj}(A,B) \) using ord_iso_is_bij, bij_is_inj
moreover
note A4
moreover from A2, A3 have \( \forall a\in C.\ r\{a\} \subseteq A \)
ultimately have \( f(\bigcap a\in C.\ r\{a\}) = ( \bigcap a\in C.\ f(r\{a\}) ) \) using inj_image_of_Inter
also
qed
from A1, A2, A3 have \( ( \bigcap a\in C.\ f(r\{a\}) ) = ( \bigcap b\in f(C).\ R\{b\} ) \) using ord_iso_pres_up_bounds
finally show \( f(\bigcap a\in C.\ r\{a\}) = (\bigcap b\in f(C).\ R\{b\}) \)
Order isomorphisms preserve completeness.
lemma ord_iso_pres_compl:
assumes A1: \( f \in ord\_iso(A,r,B,R) \) and A2: \( r \subseteq A\times A \), \( R \subseteq B\times B \) and A3: \( R \text{ is complete } \)
shows \( r \text{ is complete } \)proof{
}
fix \( C \)
assume A4: \( \text{IsBoundedAbove}(C,r) \), \( C\neq 0 \)
with A1, A2, A3 have \( \text{HasAminimum}(R,\bigcap b \in f(C).\ R\{b\}) \) using ord_iso_pres_bound_above, IsComplete_def
moreover
from A2, \( \text{IsBoundedAbove}(C,r) \) have I: \( C \subseteq A \) using Order_ZF_3_L1A
with A1, A2, \( C\neq 0 \) have \( f(\bigcap a\in C.\ r\{a\}) = (\bigcap b\in f(C).\ R\{b\}) \) using ord_iso_pres_min_up_bounds
ultimately have \( \text{HasAminimum}(R,f(\bigcap a\in C.\ r\{a\})) \)
moreover
from A2 have \( \forall a\in C.\ r\{a\} \subseteq A \)
with \( C\neq 0 \) have \( ( \bigcap a\in C.\ r\{a\} ) \subseteq A \) using ZF1_1_L7
moreover note A1, A2
ultimately have \( \text{HasAminimum}(r, \bigcap a\in C.\ r\{a\} ) \) using ord_iso_pres_has_min
then show \( r \text{ is complete } \) using IsComplete_def
qed
If the original relation is complete, then the induced one is complete.
lemma ind_rel_pres_compl:
assumes A1: \( f \in \text{bij}(A,B) \) and A2: \( R \subseteq B\times B \) and A3: \( R \text{ is complete } \)
shows \( \text{InducedRelation}(f,R) \text{ is complete } \)proof let \( r = \text{InducedRelation}(f,R) \)
from A1 have \( f \in ord\_iso(A,r,B,R) \) using bij_is_ord_iso
moreover
qed
from A1, A2 have \( r \subseteq A\times A \) using bij_is_fun, ind_rel_domain
moreover note A2, A3
ultimately show \( r \text{ is complete } \) using ord_iso_pres_compl
end
lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) 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_L10:
assumes \( \forall a\in A.\ \langle a,u\rangle \in r \)
shows \( \text{IsBoundedAbove}(A,r) \) lemma id_ord_iso: shows \( id(X) \in ord\_iso(X,r,X,r) \)
lemma single_bij_id: shows \( \text{bij}(\{x\},\{x\}) = \{id(\{x\})\} \)
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_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 \)Definition of HasAmaximum:
\( \text{HasAmaximum}(r,A) \equiv \exists M\in A.\ \forall x\in A.\ \langle x,M\rangle \in r \)
lemma max_image_ord_iso:
assumes \( \text{antisym}(r) \) and \( \text{antisym}(R) \) and \( f \in ord\_iso(A,r,B,R) \) and \( \text{HasAmaximum}(r,A) \)
shows \( \text{HasAmaximum}(R,B) \) and \( \text{Maximum}(R,B) = f( \text{Maximum}(r,A)) \) lemma inj_image_dif:
assumes \( f \in \text{inj}(A,B) \) and \( C \subseteq A \)
shows \( f(A\setminus C) = f(A)\setminus f(C) \) lemma surj_range_image_domain:
assumes \( f \in \text{surj}(A,B) \)
shows \( f(A) = B \) lemma singleton_image:
assumes \( f\in X\rightarrow Y \) and \( x\in X \)
shows \( f\{x\} = \{f(x)\} \) lemma ord_iso_rem_point:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( a \in A \)
shows \( \text{restrict}(f,A-\{a\}) \in ord\_iso(A-\{a\},r,B-\{f(a)\},R) \) lemma func1_1_L11D:
assumes \( f:X\rightarrow Y \) and \( a\notin X \) and \( g = f \cup \{\langle a,b\rangle \} \)
shows \( g : X\cup \{a\} \rightarrow Y\cup \{b\} \), \( \forall x\in X.\ g(x) = f(x) \), \( g(a) = b \) lemma bij_extend_point:
assumes \( f \in \text{bij}(X,Y) \), \( a\notin X \), \( b\notin Y \)
shows \( (f \cup \{\langle a,b\rangle \}) \in \text{bij}(X\cup \{a\},Y\cup \{b\}) \)Definition of IsLinOrder:
\( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
lemma total_is_refl:
assumes \( r \text{ is total on } X \)
shows \( \text{refl}(X,r) \) lemma ord_iso_extend:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( M_A \notin A \), \( M_B \notin B \) and \( \forall a\in A.\ \langle a, M_A\rangle \in r \), \( \forall b\in B.\ \langle b, M_B\rangle \in R \) and \( \text{antisym}(r) \), \( \text{antisym}(R) \) and \( \langle M_A,M_A\rangle \in r \longleftrightarrow \langle M_B,M_B\rangle \in R \)
shows \( f \cup \{\langle M_A,M_B\rangle \} \in ord\_iso(A\cup \{M_A\} ,r,B\cup \{M_B\} ,R) \) lemma ZF_fun_from_total:
assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \) lemma ZF_fun_from_tot_val:
assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( f(x) = b(x) \) and \( b(x)\in Y \)Definition of SliceProjection:
\( \text{SliceProjection}(X) \equiv \{\langle p,\text{fst}(p)\rangle .\ p \in X \} \)
lemma func1_1_L1:
assumes \( f:A\rightarrow C \)
shows \( domain(f) = A \)Definition of ProdFunction:
\( \text{ProdFunction}(f,g) \equiv \{\langle z,\langle f(\text{fst}(z)),g(\text{snd}(z))\rangle \rangle .\ z\in domain(f)\times domain(g)\} \)
lemma prodFunction:
assumes \( f:A\rightarrow B \), \( g:C\rightarrow D \)
shows \( \text{ProdFunction}(f,g):(A\times C)\rightarrow (B\times D) \) lemma func1_1_L15:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \) lemma prodFunctionApp:
assumes \( f:A\rightarrow B \), \( g:C\rightarrow D \), \( x\in A \), \( y\in C \)
shows \( \text{ProdFunction}(f,g)\langle x,y\rangle = \langle f(x),g(y)\rangle \)Definition of InducedRelation:
\( \text{InducedRelation}(f,R) \equiv \)
\( \{p \in domain(f)\times domain(f).\ \langle f(\text{fst}(p)),f(\text{snd}(p))\rangle \in R\} \)
lemma def_of_ind_relA:
assumes \( \langle x,y\rangle \in \text{InducedRelation}(f,R) \)
shows \( \langle f(x),f(y)\rangle \in R \) lemma def_of_ind_relB:
assumes \( f:A\rightarrow B \) and \( x\in A \), \( y\in A \) and \( \langle f(x),f(y)\rangle \in R \)
shows \( \langle x,y\rangle \in \text{InducedRelation}(f,R) \) lemma Fol1_L4:
assumes \( \text{antisym}(r) \) and \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \)
shows \( a=b \) 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 ord_iso_apply_conv:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( \langle f(x),f(y)\rangle \in R \) and \( x\in A \), \( y\in A \)
shows \( \langle x,y\rangle \in r \) 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) \)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 ord_iso_pres_antsym:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{antisym}(R) \)
shows \( \text{antisym}(r) \) lemma ord_iso_pres_trans:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{trans}(R) \)
shows \( \text{trans}(r) \) lemma ord_iso_pres_tot:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( R \text{ is total on } B \)
shows \( r \text{ is total on } A \) lemma bij_is_ord_iso:
assumes \( f \in \text{bij}(A,B) \)
shows \( f \in ord\_iso(A, \text{InducedRelation}(f,R),B,R) \) lemma domain_of_bij:
assumes \( f \in \text{bij}(X,Y) \)
shows \( domain(f) = X \) lemma ord_iso_pres_lin:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{IsLinOrder}(B,R) \)
shows \( \text{IsLinOrder}(A,r) \)Definition of IsBoundedAbove:
\( \text{IsBoundedAbove}(A,r) \equiv ( A=0 \vee (\exists u.\ \forall x\in A.\ \langle x,u\rangle \in r)) \)
lemma Order_ZF_3_L1A:
assumes \( r \subseteq X\times X \) and \( \text{IsBoundedAbove}(A,r) \)
shows \( A\subseteq X \) lemma func1_1_L15A:
assumes \( f: X\rightarrow Y \) and \( A\subseteq X \) and \( A\neq \emptyset \)
shows \( f(A) \neq \emptyset \)Definition of HasAminimum:
\( \text{HasAminimum}(r,A) \equiv \exists m\in A.\ \forall x\in A.\ \langle m,x\rangle \in r \)
lemma inj_inv_back_in_set:
assumes \( f \in \text{inj}(A,B) \) and \( C\subseteq A \) and \( y \in f(C) \)
shows \( converse(f)(y) \in C \), \( f(converse(f)(y)) = y \) lemma ord_iso_pres_rel_image:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \), \( R \subseteq B\times B \) and \( a\in A \)
shows \( f(r\{a\}) = R\{f(a)\} \) lemma inj_image_of_Inter:
assumes \( f \in \text{inj}(A,B) \) and \( I\neq \emptyset \) and \( \forall i\in I.\ P(i) \subseteq A \)
shows \( f(\bigcap i\in I.\ P(i)) = ( \bigcap i\in I.\ f(P(i)) ) \) lemma ord_iso_pres_up_bounds:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \), \( R \subseteq B\times B \) and \( C\subseteq A \)
shows \( \{f(r\{a\}).\ a\in C\} = \{R\{b\}.\ b \in f(C)\} \) lemma ord_iso_pres_bound_above:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{IsBoundedAbove}(C,r) \), \( C\neq 0 \)
shows \( \text{IsBoundedAbove}(f(C),R) \), \( f(C) \neq 0 \)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 ord_iso_pres_min_up_bounds:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \), \( R \subseteq B\times B \) and \( C\subseteq A \) and \( C\neq 0 \)
shows \( f(\bigcap a\in C.\ r\{a\}) = (\bigcap b\in f(C).\ R\{b\}) \) lemma ZF1_1_L7:
assumes \( I\neq 0 \) and \( \forall i\in I.\ P(i) \subseteq X \)
shows \( ( \bigcap i\in I.\ P(i) ) \subseteq X \) lemma ord_iso_pres_has_min:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( C\subseteq A \) and \( \text{HasAminimum}(R,f(C)) \)
shows \( \text{HasAminimum}(r,C) \) lemma ind_rel_domain:
assumes \( R \subseteq B\times B \) and \( f:A\rightarrow B \)
shows \( \text{InducedRelation}(f,R) \subseteq A\times A \) lemma ord_iso_pres_compl:
assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \), \( R \subseteq B\times B \) and \( R \text{ is complete } \)
shows \( r \text{ is complete } \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8