section ‹More on functions›
theory func_ZF_1 imports ZF.Order Order_ZF_1a func_ZF
begin
text‹In this theory we consider
some properties of functions related to order relations›
subsection‹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 ‹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
subsection‹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 ‹SliceProjection(Y×{y})›.
This is really the ZF equivalent of the meta-function ‹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
subsection‹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 ‹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 ‹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 ‹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 ‹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``(⋂a∈C. r``{a}) = (⋂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``(⋂a∈C. r``{a}) = ( ⋂a∈C. f``(r``{a}) )"
using inj_image_of_Inter by simp
also from A1 A2 A3 have
"( ⋂a∈C. f``(r``{a}) ) = ( ⋂b∈f``(C). R``{b} )"
using ord_iso_pres_up_bounds by simp
finally show "f``(⋂a∈C. r``{a}) = (⋂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,⋂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``(⋂a∈C. r``{a}) = (⋂b∈f``(C). R``{b})"
using ord_iso_pres_min_up_bounds by simp
ultimately have "HasAminimum(R,f``(⋂a∈C. r``{a}))"
by simp
moreover
from A2 have "∀a∈C. r``{a} ⊆ A"
by auto
with ‹C≠0› have "( ⋂a∈C. r``{a} ) ⊆ A" using ZF1_1_L7
by simp
moreover note A1 A2
ultimately have "HasAminimum(r, ⋂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