(*

This file is a part of IsarMathLib -

a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2008 Slawomir Kolodynski

This program is free software; Redistribution and use in source and binary forms,

with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,

this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright notice,

this list of conditions and the following disclaimer in the documentation and/or

other materials provided with the distribution.

3. The name of the author may not be used to endorse or promote products

derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED

WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF

MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.

IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,

SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,

PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;

OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,

WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR

OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,

EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.*)

header{*\isaheader{func\_ZF\_1.thy}*}

theory func_ZF_1 imports Order Order_ZF_1a func_ZF

begin

text{*In this theory we consider

some properties of functions related to order relations *}

section{*Functions and order*}

text{*This section deals with functions between ordered sets.*}

text{*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->Y" and "A⊆X" and "∀x∈A. ⟨L,f`(x)⟩ ∈ r"

shows "IsBoundedBelow(f``(A),r)"

proof -

from assms have "∀y ∈ f``(A). ⟨L,y⟩ ∈ r"

using func_imagedef by simp;

then show "IsBoundedBelow(f``(A),r)"

by (rule Order_ZF_3_L9);

qed;

text{*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->Y" and "A⊆X" and "∀x∈A. ⟨f`(x),U⟩ ∈ r"

shows "IsBoundedAbove(f``(A),r)"

proof -

from assms have "∀y ∈ f``(A). ⟨y,U⟩ ∈ r"

using func_imagedef by simp;

then show "IsBoundedAbove(f``(A),r)"

by (rule Order_ZF_3_L10);

qed;

text{*Identity is an order isomorphism.*}

lemma id_ord_iso: shows "id(X) ∈ ord_iso(X,r,X,r)"

using id_bij id_def ord_iso_def by simp;

text{*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

by auto;

text{*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: "antisym(r)" and A2: "antisym(R)" and

A3: "f ∈ ord_iso(A,r,B,R)" and

A4: "HasAmaximum(r,A)"

shows "HasAmaximum(R,B)" and "Maximum(R,B) = f`(Maximum(r,A))"

proof -

let ?M = "Maximum(r,A)"

from A1 A4 have "?M ∈ A" using Order_ZF_4_L3 by simp;

from A3 have "f:A->B" using ord_iso_def bij_is_fun

by simp;

with `?M ∈ A` have I: "f`(?M) ∈ B"

using apply_funtype by simp;

{ fix y assume "y ∈ B"

let ?x = "converse(f)`(y)"

from A3 have "converse(f) ∈ ord_iso(B,R,A,r)"

using ord_iso_sym by simp;

then have "converse(f): B -> A"

using ord_iso_def bij_is_fun by simp;

with `y ∈ B` have "?x ∈ A"

by simp;

with A1 A3 A4 `?x ∈ A` `?M ∈ A` have "⟨f`(?x), f`(?M)⟩ ∈ R"

using Order_ZF_4_L3 ord_iso_apply by simp;

with A3 `y ∈ B` have "⟨y, f`(?M)⟩ ∈ R"

using right_inverse_bij ord_iso_def by auto;

} then have II: "∀y ∈ B. ⟨y, f`(?M)⟩ ∈ R" by simp;

with A2 I show "Maximum(R,B) = f`(?M)"

by (rule Order_ZF_4_L14)

from I II show "HasAmaximum(R,B)"

using HasAmaximum_def by auto;

qed;

text{*Maximum is a fixpoint of order automorphism.*}

lemma max_auto_fixpoint:

assumes "antisym(r)" and "f ∈ ord_iso(A,r,A,r)"

and "HasAmaximum(r,A)"

shows "Maximum(r,A) = f`(Maximum(r,A))"

using assms max_image_ord_iso by blast;

text{*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 ∈ ord_iso(A,r,B,R)" and A2: "a ∈ A"

shows "restrict(f,A-{a}) ∈ ord_iso(A-{a},r,B-{f`(a)},R)"

proof -

let ?f⇩_{0}= "restrict(f,A-{a})"

have "A-{a} ⊆ A" by auto;

with A1 have "?f⇩_{0}∈ ord_iso(A-{a},r,f``(A-{a}),R)"

using ord_iso_restrict_image by simp;

moreover

from A1 have "f ∈ inj(A,B)"

using ord_iso_def bij_def by simp;

with A2 have "f``(A-{a}) = f``(A) - f``{a}"

using inj_image_dif by simp;

moreover from A1 have "f``(A) = B"

using ord_iso_def bij_def surj_range_image_domain

by auto;

moreover

from A1 have "f: A->B"

using ord_iso_def bij_is_fun by simp;

with A2 have "f``{a} = {f`(a)}"

using singleton_image by simp;

ultimately show ?thesis by simp;

qed;

text{*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: "antisym(r)" and "f ∈ ord_iso(A,r,B,R)" and

A4: "HasAmaximum(r,A)" and A5: "M = Maximum(r,A)"

shows "restrict(f,A-{M}) ∈ ord_iso(A-{M}, r, B-{f`(M)},R)"

using assms Order_ZF_4_L3 ord_iso_rem_point by simp;

text{*Lemma about extending order isomorphisms by adding one point

to the domain.*}

lemma ord_iso_extend: assumes A1: "f ∈ ord_iso(A,r,B,R)" and

A2: "M⇩_{A}∉ A" "M⇩_{B}∉ B" and

A3: "∀a∈A. ⟨a, M⇩_{A}⟩ ∈ r" "∀b∈B. ⟨b, M⇩_{B}⟩ ∈ R" and

A4: "antisym(r)" "antisym(R)" and

A5: "⟨M⇩_{A},M⇩_{A}⟩ ∈ r <-> ⟨M⇩_{B},M⇩_{B}⟩ ∈ R"

shows "f ∪ {⟨ M⇩_{A},M⇩_{B}⟩} ∈ ord_iso(A∪{M⇩_{A}} ,r,B∪{M⇩_{B}} ,R)"

proof -

let ?g = "f ∪ {⟨ M⇩_{A},M⇩_{B}⟩}"

from A1 A2 have

"?g : A∪{M⇩_{A}} -> B∪{M⇩_{B}}" and

I: "∀x∈A. ?g`(x) = f`(x)" and II: "?g`(M⇩_{A}) = M⇩_{B}"

using ord_iso_def bij_def inj_def func1_1_L11D

by auto;

from A1 A2 have "?g ∈ bij(A∪{M⇩_{A}},B∪{M⇩_{B}}) "

using ord_iso_def bij_extend_point by simp;

moreover have "∀x ∈ A∪{M⇩_{A}}. ∀ y ∈ A∪{M⇩_{A}}.

⟨x,y⟩ ∈ r <-> ⟨?g`(x), ?g`(y)⟩ ∈ R"

proof -

{ fix x y

assume "x ∈ A∪{M⇩_{A}}" and "y ∈ A∪{M⇩_{A}}"

then have "x∈A ∧ y ∈ A ∨ x∈A ∧ y = M⇩_{A}∨

x = M⇩_{A}∧ y ∈ A ∨ x = M⇩_{A}∧ y = M⇩_{A}"

by auto;

moreover

{ assume "x∈A ∧ y ∈ A"

with A1 I have "⟨x,y⟩ ∈ r <-> ⟨?g`(x), ?g`(y)⟩ ∈ R"

using ord_iso_def by simp }

moreover

{ assume "x∈A ∧ y = M⇩_{A}"

with A1 A3 I II have "⟨x,y⟩ ∈ r <-> ⟨?g`(x), ?g`(y)⟩ ∈ R"

using ord_iso_def bij_def inj_def apply_funtype

by auto }

moreover

{ assume "x = M⇩_{A}∧ y ∈ A"

with A2 A3 A4 have "⟨x,y⟩ ∉ r"

using antisym_def by auto;

moreover

{ assume A6: "⟨?g`(x), ?g`(y)⟩ ∈ R"

from A1 I II `x = M⇩_{A}∧ y ∈ A` have

III: "?g`(y) ∈ B" "?g`(x) = M⇩_{B}"

using ord_iso_def bij_def inj_def apply_funtype

by auto;

with A3 have "⟨?g`(y), ?g`(x)⟩ ∈ R" by simp

with A4 A6 have "?g`(y) = ?g`(x)" using antisym_def

by auto;

with A2 III have False by simp;

} hence "⟨?g`(x), ?g`(y)⟩ ∉ R" by auto;

ultimately have "⟨x,y⟩ ∈ r <-> ⟨?g`(x), ?g`(y)⟩ ∈ R"

by simp }

moreover

{ assume "x = M⇩_{A}∧ y = M⇩_{A}"

with A5 II have "⟨x,y⟩ ∈ r <-> ⟨?g`(x), ?g`(y)⟩ ∈ R"

by simp }

ultimately have "⟨x,y⟩ ∈ r <-> ⟨?g`(x), ?g`(y)⟩ ∈ R"

by auto;

} thus ?thesis by auto;

qed;

ultimately show ?thesis using ord_iso_def

by simp;

qed;

text{*A kind of converse to @{text "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: "IsLinOrder(X,r)" "IsLinOrder(Y,R)" and

A2: "HasAmaximum(r,X)" "HasAmaximum(R,Y)"

"ord_iso(X - {Maximum(r,X)},r,Y - {Maximum(R,Y)},R) ≠ 0"

shows "ord_iso(X,r,Y,R) ≠ 0"

proof -

let ?M⇩_{A}= "Maximum(r,X)"

let ?A = "X - {?M⇩_{A}}"

let ?M⇩_{B}= "Maximum(R,Y)"

let ?B = "Y - {?M⇩_{B}}"

from A2 obtain f where "f ∈ ord_iso(?A,r,?B,R)"

by auto;

moreover have "?M⇩_{A}∉ ?A" and "?M⇩_{B}∉ ?B"

by auto;

moreover from A1 A2 have

"∀a∈?A. ⟨a,?M⇩_{A}⟩ ∈ r" and "∀b∈?B. ⟨b,?M⇩_{B}⟩ ∈ R"

using IsLinOrder_def Order_ZF_4_L3 by auto;

moreover from A1 have "antisym(r)" and "antisym(R)"

using IsLinOrder_def by auto;

moreover from A1 A2 have "⟨?M⇩_{A},?M⇩_{A}⟩ ∈ r <-> ⟨?M⇩_{B},?M⇩_{B}⟩ ∈ R"

using IsLinOrder_def Order_ZF_4_L3 IsLinOrder_def

total_is_refl refl_def by auto;

ultimately have

"f ∪ {⟨ ?M⇩_{A},?M⇩_{B}⟩} ∈ ord_iso(?A∪{?M⇩_{A}} ,r,?B∪{?M⇩_{B}} ,R)"

by (rule ord_iso_extend);

moreover from A1 A2 have

"?A∪{?M⇩_{A}} = X" and "?B∪{?M⇩_{B}} = Y"

using IsLinOrder_def Order_ZF_4_L3 by auto;

ultimately show "ord_iso(X,r,Y,R) ≠ 0"

using ord_iso_extend by auto;

qed;

section{*Projections in cartesian products*}

text{*In this section we consider maps arising naturally

in cartesian products. *}

text{*There is a natural bijection etween $X=Y\times \{ y\}$ (a "slice")

and $Y$.

We will call this the @{text "SliceProjection(Y×{y})"}.

This is really the ZF equivalent of the meta-function @{text "fst(x)"}.

*}

definition

"SliceProjection(X) ≡ {⟨p,fst(p)⟩. p ∈ X }"

text{*A slice projection is a bijection between $X\times\{ y\}$ and $X$.*}

lemma slice_proj_bij: shows

"SliceProjection(X×{y}): X×{y} -> X"

"domain(SliceProjection(X×{y})) = X×{y}"

"∀p∈X×{y}. SliceProjection(X×{y})`(p) = fst(p)"

"SliceProjection(X×{y}) ∈ bij(X×{y},X)"

proof -

let ?P = "SliceProjection(X×{y})"

have "∀p ∈ X×{y}. fst(p) ∈ X" by simp;

moreover from this have

"{⟨p,fst(p)⟩. p ∈ X×{y} } : X×{y} -> X"

by (rule ZF_fun_from_total);

ultimately show

I: "?P: X×{y} -> X" and II: "∀p∈X×{y}. ?P`(p) = fst(p)"

using ZF_fun_from_tot_val SliceProjection_def by auto;

hence

"∀a ∈ X×{y}. ∀ b ∈ X×{y}. ?P`(a) = ?P`(b) --> a=b"

by auto;

with I have "?P ∈ inj(X×{y},X)" using inj_def

by simp;

moreover from II have "∀x∈X. ∃p∈X×{y}. ?P`(p) = x"

by simp;

with I have "?P ∈ surj(X×{y},X)" using surj_def

by simp;

ultimately show "?P ∈ bij(X×{y},X)"

using bij_def by simp;

from I show "domain(SliceProjection(X×{y})) = X×{y}"

using func1_1_L1 by simp

qed;

section{*Induced relations and order isomorphisms *}

text{*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 @{text "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.*}

text{*We call the relation created by a relation on $Y$ and a mapping

$f:X\rightarrow Y$ the @{text "InducedRelation(f,R)"}.*}

definition

"InducedRelation(f,R) ≡

{p ∈ domain(f)×domain(f). ⟨f`(fst(p)),f`(snd(p))⟩ ∈ R}"

text{*A reformulation of the definition of the relation induced by

a function.*}

lemma def_of_ind_relA:

assumes "⟨x,y⟩ ∈ InducedRelation(f,R)"

shows "⟨f`(x),f`(y)⟩ ∈ R"

using assms InducedRelation_def by simp;

text{*A reformulation of the definition of the relation induced by

a function, kind of converse of @{text "def_of_ind_relA"}.*}

lemma def_of_ind_relB: assumes "f:A->B" and

"x∈A" "y∈A" and "⟨f`(x),f`(y)⟩ ∈ R"

shows "⟨x,y⟩ ∈ InducedRelation(f,R)"

using assms func1_1_L1 InducedRelation_def by simp;

text{*A property of order isomorphisms that is missing from

standard Isabelle's @{text "Order.thy"}.*}

lemma ord_iso_apply_conv:

assumes "f ∈ ord_iso(A,r,B,R)" and

"⟨f`(x),f`(y)⟩ ∈ R" and "x∈A" "y∈A"

shows "⟨x,y⟩ ∈ r"

using assms ord_iso_def by simp;

text{*The next lemma tells us where the induced relation is defined*}

lemma ind_rel_domain:

assumes "R ⊆ B×B" and "f:A->B"

shows "InducedRelation(f,R) ⊆ A×A"

using assms func1_1_L1 InducedRelation_def

by auto;

text{*A bijection is an order homomorphisms between a relation

and the induced one.*}

lemma bij_is_ord_iso: assumes A1: "f ∈ bij(A,B)"

shows "f ∈ ord_iso(A,InducedRelation(f,R),B,R)"

proof -

let ?r = "InducedRelation(f,R)"

{ fix x y assume A2: "x∈A" "y∈A"

have "⟨x,y⟩ ∈ ?r <-> ⟨f`(x),f`(y)⟩ ∈ R"

proof;

assume "⟨x,y⟩ ∈ ?r" then show "⟨f`(x),f`(y)⟩ ∈ R"

using def_of_ind_relA by simp;

next assume "⟨f`(x),f`(y)⟩ ∈ R"

with A1 A2 show "⟨x,y⟩ ∈ ?r"

using bij_is_fun def_of_ind_relB by blast

qed }

with A1 show "f ∈ ord_iso(A,InducedRelation(f,R),B,R)"

using ord_isoI by simp

qed;

text{*An order isomoprhism preserves antisymmetry.*}

lemma ord_iso_pres_antsym: assumes A1: "f ∈ ord_iso(A,r,B,R)" and

A2: "r ⊆ A×A" and A3: "antisym(R)"

shows "antisym(r)"

proof -

{ fix x y

assume A4: "⟨x,y⟩ ∈ r" "⟨y,x⟩ ∈ r"

from A1 have "f ∈ inj(A,B)"

using ord_iso_is_bij bij_is_inj by simp

moreover

from A1 A2 A4 have

"⟨f`(x), f`(y)⟩ ∈ R" and "⟨f`(y), f`(x)⟩ ∈ R"

using ord_iso_apply by auto;

with A3 have "f`(x) = f`(y)" by (rule Fol1_L4);

moreover from A2 A4 have "x∈A" "y∈A" by auto;

ultimately have "x=y" by (rule inj_apply_equality);

} then have "∀x y. ⟨x,y⟩ ∈ r ∧ ⟨y,x⟩ ∈ r --> x=y" by auto;

then show "antisym(r)" using imp_conj antisym_def

by simp;

qed;

text{*Order isomoprhisms preserve transitivity.*}

lemma ord_iso_pres_trans: assumes A1: "f ∈ ord_iso(A,r,B,R)" and

A2: "r ⊆ A×A" and A3: "trans(R)"

shows "trans(r)"

proof -

{ fix x y z

assume A4: "⟨x, y⟩ ∈ r" "⟨y, z⟩ ∈ r"

note A1

moreover

from A1 A2 A4 have

"⟨f`(x), f`(y)⟩ ∈ R ∧ ⟨f`(y), f`(z)⟩ ∈ R"

using ord_iso_apply by auto;

with A3 have "⟨f`(x),f`(z)⟩ ∈ R" by (rule Fol1_L3);

moreover from A2 A4 have "x∈A" "z∈A" by auto;

ultimately have "⟨x, z⟩ ∈ r" using ord_iso_apply_conv

by simp;

} then have "∀ x y z. ⟨x, y⟩ ∈ r ∧ ⟨y, z⟩ ∈ r --> ⟨x, z⟩ ∈ r"

by blast;

then show "trans(r)" by (rule Fol1_L2);

qed;

text{*Order isomorphisms preserve totality.*}

lemma ord_iso_pres_tot: assumes A1: "f ∈ ord_iso(A,r,B,R)" and

A2: "r ⊆ A×A" and A3: "R {is total on} B"

shows "r {is total on} A"

proof -

{ fix x y

assume "x∈A" "y∈A" "⟨x,y⟩ ∉ r"

with A1 have "⟨f`(x),f`(y)⟩ ∉ R" using ord_iso_apply_conv

by auto;

moreover

from A1 have "f:A->B" using ord_iso_is_bij bij_is_fun

by simp;

with A3 `x∈A` `y∈A` have

"⟨f`(x),f`(y)⟩ ∈ R ∨ ⟨f`(y),f`(x)⟩ ∈ R"

using apply_funtype IsTotal_def by simp;

ultimately have "⟨f`(y),f`(x)⟩ ∈ R" by simp;

with A1 `x∈A` `y∈A` have "⟨y,x⟩ ∈ r"

using ord_iso_apply_conv by simp;

} then have "∀x∈A. ∀y∈A. ⟨x,y⟩ ∈ r ∨ ⟨y,x⟩ ∈ r"

by blast;

then show "r {is total on} A" using IsTotal_def

by simp;

qed;

text{*Order isomorphisms preserve linearity.*}

lemma ord_iso_pres_lin: assumes "f ∈ ord_iso(A,r,B,R)" and

"r ⊆ A×A" and "IsLinOrder(B,R)"

shows "IsLinOrder(A,r)"

using assms ord_iso_pres_antsym ord_iso_pres_trans ord_iso_pres_tot

IsLinOrder_def by simp;

text{*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 ∈ bij(A,B)" and A2: "IsLinOrder(B,R)"

shows "IsLinOrder(A,InducedRelation(f,R))"

proof -

let ?r = "InducedRelation(f,R)"

from A1 have "f ∈ ord_iso(A,?r,B,R)" and "?r ⊆ A×A"

using bij_is_ord_iso domain_of_bij InducedRelation_def

by auto;

with A2 show "IsLinOrder(A,?r)" using ord_iso_pres_lin

by simp;

qed;

text{*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 ∈ ord_iso(A,r,B,R)" and A2: "r ⊆ A×A" and

A3: "IsBoundedAbove(C,r)" "C≠0"

shows "IsBoundedAbove(f``(C),R)" "f``(C) ≠ 0"

proof -

from A3 obtain u where I: "∀x∈C. ⟨x,u⟩ ∈ r"

using IsBoundedAbove_def by auto;

from A1 have "f:A->B" using ord_iso_is_bij bij_is_fun

by simp;

from A2 A3 have "C⊆A" using Order_ZF_3_L1A by blast;

from A3 obtain x where "x∈C" by auto;

with A2 I have "u∈A" by auto;

{ fix y assume "y ∈ f``(C)"

with `f:A->B` `C⊆A` obtain x where "x∈C" and "y = f`(x)"

using func_imagedef by auto;

with A1 I `C⊆A` `u∈A` have "⟨y,f`(u)⟩ ∈ R"

using ord_iso_apply by auto;

} then have "∀y ∈ f``(C). ⟨y,f`(u)⟩ ∈ R" by simp;

then show "IsBoundedAbove(f``(C),R)" by (rule Order_ZF_3_L10);

from A3 `f:A->B` `C⊆A` show "f``(C) ≠ 0" using func1_1_L15A

by simp;

qed;

text{*Order isomorphisms preserve the property of having a minimum.*}

lemma ord_iso_pres_has_min:

assumes A1: "f ∈ ord_iso(A,r,B,R)" and A2: "r ⊆ A×A" and

A3: "C⊆A" and A4: "HasAminimum(R,f``(C))"

shows "HasAminimum(r,C)"

proof -

from A4 obtain m where

I: "m ∈ f``(C)" and II: "∀y ∈ f``(C). ⟨m,y⟩ ∈ R"

using HasAminimum_def by auto;

let ?k = "converse(f)`(m)"

from A1 have "f:A->B" using ord_iso_is_bij bij_is_fun

by simp

from A1 have "f ∈ inj(A,B)" using ord_iso_is_bij bij_is_inj

by simp;

with A3 I have "?k ∈ C" and III: "f`(?k) = m"

using inj_inv_back_in_set by auto;

moreover

{ fix x assume A5: "x∈C"

with A3 II `f:A->B` `?k ∈ C` III have

"?k ∈ A" "x∈A" "⟨f`(?k),f`(x)⟩ ∈ R"

using func_imagedef by auto;

with A1 have "⟨?k,x⟩ ∈ r" using ord_iso_apply_conv

by simp;

} then have "∀x∈C. ⟨?k,x⟩ ∈ r" by simp;

ultimately show "HasAminimum(r,C)" using HasAminimum_def by auto;

qed;

text{*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 ∈ ord_iso(A,r,B,R)" and

A2: "r ⊆ A×A" "R ⊆ B×B" and

A3: "a∈A"

shows "f``(r``{a}) = R``{f`(a)}"

proof;

from A1 have "f:A->B" using ord_iso_is_bij bij_is_fun

by simp;

moreover from A2 A3 have I: "r``{a} ⊆ A" by auto;

ultimately have I: "f``(r``{a}) = {f`(x). x ∈ r``{a} }"

using func_imagedef by simp;

{ fix y assume A4: "y ∈ f``(r``{a})"

with I obtain x where

"x ∈ r``{a}" and II: "y = f`(x)"

by auto;

with A1 A2 have "⟨f`(a),f`(x)⟩ ∈ R" using ord_iso_apply

by auto;

with II have "y ∈ R``{f`(a)}" by auto;

} then show "f``(r``{a}) ⊆ R``{f`(a)}" by auto;

{ fix y assume A5: "y ∈ R``{f`(a)}"

let ?x = "converse(f)`(y)"

from A2 A5 have

"⟨f`(a),y⟩ ∈ R" "f`(a) ∈ B" and IV: "y∈B"

by auto;

with A1 have III: "⟨converse(f)`(f`(a)),?x⟩ ∈ r"

using ord_iso_converse by simp;

moreover from A1 A3 have "converse(f)`(f`(a)) = a"

using ord_iso_is_bij left_inverse_bij by blast;

ultimately have "f`(?x) ∈ {f`(x). x ∈ r``{a} }"

by auto;

moreover from A1 IV have "f`(?x) = y"

using ord_iso_is_bij right_inverse_bij by blast;

moreover from A1 I have "f``(r``{a}) = {f`(x). x ∈ r``{a} }"

using ord_iso_is_bij bij_is_fun func_imagedef by blast;

ultimately have "y ∈ f``(r``{a})" by simp;

} then show "R``{f`(a)} ⊆ f``(r``{a})" by auto;

qed;

text{*Order isomorphisms preserve collections of upper bounds.*}

lemma ord_iso_pres_up_bounds:

assumes A1: "f ∈ ord_iso(A,r,B,R)" and

A2: "r ⊆ A×A" "R ⊆ B×B" and

A3: "C⊆A"

shows "{f``(r``{a}). a∈C} = {R``{b}. b ∈ f``(C)}"

proof;

from A1 have "f:A->B"

using ord_iso_is_bij bij_is_fun by simp

{ fix Y assume "Y ∈ {f``(r``{a}). a∈C}"

then obtain a where "a∈C" and I: "Y = f``(r``{a})"

by auto;

from A3 `a∈C` have "a∈A" by auto;

with A1 A2 have "f``(r``{a}) = R``{f`(a)}"

using ord_iso_pres_rel_image by simp;

moreover from A3 `f:A->B` `a∈C` have "f`(a) ∈ f``(C)"

using func_imagedef by auto;

ultimately have "f``(r``{a}) ∈ { R``{b}. b ∈ f``(C) }"

by auto;

with I have "Y ∈ { R``{b}. b ∈ f``(C) }" by simp;

} then show "{f``(r``{a}). a∈C} ⊆ {R``{b}. b ∈ f``(C)}"

by blast;

{ fix Y assume "Y ∈ {R``{b}. b ∈ f``(C)}"

then obtain b where "b ∈ f``(C)" and II: "Y = R``{b}"

by auto;

with A3 `f:A->B` obtain a where "a∈C" and "b = f`(a)"

using func_imagedef by auto;

with A3 II have "a∈A" and "Y = R``{f`(a)}" by auto;

with A1 A2 have "Y = f``(r``{a})"

using ord_iso_pres_rel_image by simp;

with `a∈C` have "Y ∈ {f``(r``{a}). a∈C}" by auto;

} then show "{R``{b}. b ∈ f``(C)} ⊆ {f``(r``{a}). a∈C}"

by auto;

qed;

text{*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 ∈ ord_iso(A,r,B,R)" and A2: "r ⊆ A×A" "R ⊆ B×B" and

A3: "C⊆A" and A4: "C≠0"

shows "f``(\<Inter>a∈C. r``{a}) = (\<Inter>b∈f``(C). R``{b})"

proof -

from A1 have "f ∈ inj(A,B)"

using ord_iso_is_bij bij_is_inj by simp;

moreover note A4

moreover from A2 A3 have "∀a∈C. r``{a} ⊆ A" by auto;

ultimately have

"f``(\<Inter>a∈C. r``{a}) = ( \<Inter>a∈C. f``(r``{a}) )"

using inj_image_of_Inter by simp;

also from A1 A2 A3 have

"( \<Inter>a∈C. f``(r``{a}) ) = ( \<Inter>b∈f``(C). R``{b} )"

using ord_iso_pres_up_bounds by simp;

finally show "f``(\<Inter>a∈C. r``{a}) = (\<Inter>b∈f``(C). R``{b})"

by simp;

qed;

text{*Order isomorphisms preserve completeness.*}

lemma ord_iso_pres_compl:

assumes A1: "f ∈ ord_iso(A,r,B,R)" and

A2: "r ⊆ A×A" "R ⊆ B×B" and A3: "R {is complete}"

shows "r {is complete}"

proof -

{ fix C

assume A4: "IsBoundedAbove(C,r)" "C≠0"

with A1 A2 A3 have

"HasAminimum(R,\<Inter>b ∈ f``(C). R``{b})"

using ord_iso_pres_bound_above IsComplete_def

by simp;

moreover

from A2 `IsBoundedAbove(C,r)` have I: "C ⊆ A" using Order_ZF_3_L1A

by blast;

with A1 A2 `C≠0` have "f``(\<Inter>a∈C. r``{a}) = (\<Inter>b∈f``(C). R``{b})"

using ord_iso_pres_min_up_bounds by simp;

ultimately have "HasAminimum(R,f``(\<Inter>a∈C. r``{a}))"

by simp;

moreover

from A2 have "∀a∈C. r``{a} ⊆ A"

by auto;

with `C≠0` have "( \<Inter>a∈C. r``{a} ) ⊆ A" using ZF1_1_L7

by simp;

moreover note A1 A2

ultimately have "HasAminimum(r, \<Inter>a∈C. r``{a} )"

using ord_iso_pres_has_min by simp;

} then show "r {is complete}" using IsComplete_def

by simp;

qed;

text{*If the original relation is complete, then the induced

one is complete.*}

lemma ind_rel_pres_compl: assumes A1: "f ∈ bij(A,B)"

and A2: "R ⊆ B×B" and A3: "R {is complete}"

shows "InducedRelation(f,R) {is complete}"

proof -

let ?r = "InducedRelation(f,R)"

from A1 have "f ∈ ord_iso(A,?r,B,R)"

using bij_is_ord_iso by simp;

moreover from A1 A2 have "?r ⊆ A×A"

using bij_is_fun ind_rel_domain by simp;

moreover note A2 A3

ultimately show "?r {is complete}"

using ord_iso_pres_compl by simp;

qed;

end