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