# IsarMathLib

## A library of formalized mathematics for Isabelle/ZF theorem proving environment

theory func_ZF_1 imports Order Order_ZF_1a func_ZF
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_def

Identity 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_id

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

If 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
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$$
qed

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_point

Lemma 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
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
{
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 {
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
} moreover {
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
} moreover {
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$$
} moreover {
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$$
} ultimately have $$\langle x,y\rangle \in r \longleftrightarrow \langle g(x), g(y)\rangle \in R$$
}
thus $$thesis$$
qed
ultimately show $$thesis$$ using ord_iso_def
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
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
qed

### Projections 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

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

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

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

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

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

If 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 {
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
qed

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
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\})$$
qed

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
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
qed
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-C) = f(A) - 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)$$
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 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 0$$

shows $$f(A) \neq 0$$
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 0$$ 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 }$$
198
84
39
39