Theory MetricSpace_ZF
section ‹ Metric spaces ›
theory MetricSpace_ZF imports Topology_ZF_1 OrderedLoop_ZF Lattice_ZF
begin
text‹A metric space is a set on which a distance between points is defined as a function
$d:X \times X \to [0,\infty)$. With this definition each metric space is a topological space
which is paracompact and Hausdorff ($T_2$), hence normal (in fact even perfectly normal).›
subsection‹ Pseudometric - definition and basic properties ›
text‹A metric on $X$ is usually defined as a function $d:X \times X \to [0,\infty)$ that satisfies
the conditions $d(x,x) = 0$, $d(x, y) = 0 \Rightarrow x = y$ (identity of indiscernibles),
$d(x, y) = d(y, x)$ (symmetry) and $d(x, y) \le d(x, z) + d(z, y)$ (triangle inequality)
for all $x,y \in X$. Here we are going to be a bit more general and define metric and
pseudo-metric as a function valued in an ordered loop. ›
text‹ First we define a pseudo-metric, which has the axioms of a metric, but without the second part
of the identity of indiscernibles. In our definition ‹IsApseudoMetric› is a predicate on five sets: the function $d$,
the set $X$ on which the metric is defined, the loop carrier $G$, the loop operation $A$
and the order $r$ on $G$.›
definition
"IsApseudoMetric(d,X,G,A,r) ≡ d:X×X → Nonnegative(G,A,r)
∧ (∀x∈X. d`⟨x,x⟩ = TheNeutralElement(G,A))
∧ (∀x∈X.∀y∈X. d`⟨x,y⟩ = d`⟨y,x⟩)
∧ (∀x∈X.∀y∈X.∀z∈X. ⟨d`⟨x,z⟩, A`⟨d`⟨x,y⟩,d`⟨y,z⟩⟩⟩ ∈ r)"
text‹We add the full axiom of identity of indiscernibles to the definition of a pseudometric
to get the definition of metric.›
definition
"IsAmetric(d,X,G,A,r) ≡
IsApseudoMetric(d,X,G,A,r) ∧ (∀x∈X.∀y∈X. d`⟨x,y⟩ = TheNeutralElement(G,A) ⟶ x=y)"
text‹A disk is defined as set of points located less than the radius from the center.›
definition "Disk(X,d,r,c,R) ≡ {x∈X. ⟨d`⟨c,x⟩,R⟩ ∈ StrictVersion(r)}"
text‹Next we define notation for metric spaces. We will reuse the additive notation defined in
the ‹loop1› locale adding only the assumption about $d$ being a pseudometric and notation
for a disk centered at $c$ with radius $R$.
Since for many theorems it is sufficient to assume the pseudometric axioms we will
assume in this context that the sets $d,X,L,A,r$ form a pseudometric raher than a metric.›
locale pmetric_space = loop1 +
fixes d and X
assumes pmetricAssum: "IsApseudoMetric(d,X,L,A,r)"
fixes disk
defines disk_def [simp]: "disk(c,R) ≡ Disk(X,d,r,c,R)"
text‹ The next lemma shows the definition of the pseudometric in the notation used in the
‹metric_space› context.›
lemma (in pmetric_space) pmetric_properties: shows
"d: X×X → L⇧+"
"∀x∈X. d`⟨x,x⟩ = 𝟬"
"∀x∈X.∀y∈X. d`⟨x,y⟩ = d`⟨y,x⟩"
"∀x∈X.∀y∈X.∀z∈X. d`⟨x,z⟩ \<lsq> d`⟨x,y⟩ \<ra> d`⟨y,z⟩"
using pmetricAssum unfolding IsApseudoMetric_def by auto
text‹The values of the metric are in the loop.›
lemma (in pmetric_space) pmetric_loop_valued: assumes "x∈X" "y∈X"
shows "d`⟨x,y⟩ ∈ L⇧+" "d`⟨x,y⟩ ∈ L"
proof -
from assms show "d`⟨x,y⟩ ∈ L⇧+" using pmetric_properties(1) apply_funtype
by simp
then show "d`⟨x,y⟩ ∈ L" using Nonnegative_def by auto
qed
text‹The definition of the disk in the notation used in the ‹pmetric_space› context:›
lemma (in pmetric_space) disk_definition: shows "disk(c,R) = {x∈X. d`⟨c,x⟩ \<ls> R}"
proof -
have "disk(c,R) = Disk(X,d,r,c,R)" by simp
then have "disk(c,R) = {x∈X. ⟨d`⟨c,x⟩,R⟩ ∈ StrictVersion(r)}" unfolding Disk_def by simp
moreover have "∀x∈X. ⟨d`⟨c,x⟩,R⟩ ∈ StrictVersion(r) ⟷ d`⟨c,x⟩ \<ls> R"
using def_of_strict_ver by simp
ultimately show ?thesis by auto
qed
text‹If the radius is positive then the center is in disk.›
lemma (in pmetric_space) center_in_disk: assumes "c∈X" and "R∈L⇩+" shows "c ∈ disk(c,R)"
using pmetricAssum assms IsApseudoMetric_def PositiveSet_def disk_definition by simp
text‹A technical lemma that allows us to shorten some proofs: ›
lemma (in pmetric_space) radius_in_loop: assumes "c∈X" and "x ∈ disk(c,R)"
shows "R∈L" "𝟬\<ls>R" "R∈L⇩+" "(\<rm>d`⟨c,x⟩ \<ad> R) ∈ L⇩+"
proof -
from assms(2) have "x∈X" and "d`⟨c,x⟩ \<ls> R" using disk_definition by auto
with assms(1) show "𝟬\<ls>R" using pmetric_properties(1) apply_funtype
nonneg_definition loop_strict_ord_trans by blast
then show "R∈L" and "R∈L⇩+" using posset_definition PositiveSet_def by auto
from ‹d`⟨c,x⟩ \<ls> R› show "(\<rm>d`⟨c,x⟩ \<ad> R) ∈ L⇩+"
using ls_other_side(2) by simp
qed
text‹If a point $x$ is inside a disk $B$ and $m\leq R-d(c,x)$ then the disk centered
at the point $x$ and with radius $m$ is contained in the disk $B$. ›
lemma (in pmetric_space) disk_in_disk:
assumes "c∈X" and "x ∈ disk(c,R)" and "m \<lsq> (\<rm>d`⟨c,x⟩ \<ad> R)"
shows "disk(x,m) ⊆ disk(c,R)"
proof
fix y assume "y ∈ disk(x,m)"
then have "d`⟨x,y⟩ \<ls> m" using disk_definition by simp
from assms(1,2) ‹y ∈ disk(x,m)› have "R∈L" "x∈X" "y∈X"
using radius_in_loop(1) disk_definition by auto
with assms(1) have "d`⟨c,y⟩ \<lsq> d`⟨c,x⟩ \<ra> d`⟨x,y⟩" using pmetric_properties(4) by simp
from assms(1) ‹x∈X› have "d`⟨c,x⟩ ∈ L"
using pmetric_properties(1) apply_funtype nonneg_subset by auto
with ‹d`⟨x,y⟩ \<ls> m› assms(3) have "d`⟨c,x⟩ \<ra> d`⟨x,y⟩ \<ls> d`⟨c,x⟩ \<ra> (\<rm>d`⟨c,x⟩ \<ad> R)"
using loop_strict_ord_trans1 strict_ord_trans_inv(2) by blast
with ‹d`⟨c,x⟩ ∈ L› ‹R∈L› ‹d`⟨c,y⟩ \<lsq> d`⟨c,x⟩ \<ra> d`⟨x,y⟩› ‹y∈X› show "y ∈ disk(c,R)"
using lrdiv_props(6) loop_strict_ord_trans disk_definition by simp
qed
text‹ If we assume that the order on the group makes the positive set a meet semi-lattice (i.e.
every two-element subset of $G_+$ has a greatest lower bound) then
the collection of disks centered at points of the space and with radii in the positive set
of the group satisfies the base condition. The meet semi-lattice assumption can be weakened
to "each two-element subset of $G_+$ has a lower bound in $G_+$", but we don't do that here. ›
lemma (in pmetric_space) disks_form_base:
assumes "r {down-directs} L⇩+"
defines "B ≡ ⋃c∈X. {disk(c,R). R∈L⇩+}"
shows "B {satisfies the base condition}"
proof -
{ fix U V assume "U∈B" "V∈B"
fix x assume "x∈U∩V"
have "∃W∈B. x∈W ∧ W⊆U∩V"
proof -
from assms(2) ‹U∈B› ‹V∈B› obtain c⇩U c⇩V R⇩U R⇩V
where "c⇩U ∈ X" "R⇩U ∈ L⇩+" "c⇩V ∈ X" "R⇩V ∈ L⇩+" "U = disk(c⇩U,R⇩U)" "V = disk(c⇩V,R⇩V)"
by auto
with ‹x∈U∩V› have "x ∈ disk(c⇩U,R⇩U)" and "x ∈ disk(c⇩V,R⇩V)" by auto
then have "x∈X" "d`⟨c⇩U,x⟩ \<ls> R⇩U" "d`⟨c⇩V,x⟩ \<ls> R⇩V" using disk_definition by auto
let ?m⇩U = "\<rm> d`⟨c⇩U,x⟩ \<ad> R⇩U"
let ?m⇩V = "\<rm> d`⟨c⇩V,x⟩ \<ad> R⇩V"
from ‹c⇩U∈X› ‹x∈disk(c⇩U,R⇩U)› ‹c⇩V∈X› ‹x∈disk(c⇩V,R⇩V)› have "?m⇩U∈L⇩+" and "?m⇩V∈L⇩+"
using radius_in_loop(4) by auto
with assms(1) obtain m where "m ∈ L⇩+" "m \<lsq> ?m⇩U" "m \<lsq> ?m⇩V"
unfolding DownDirects_def by auto
let ?W = "disk(x,m)"
from ‹m ∈ L⇩+› ‹m \<lsq> ?m⇩U› ‹m \<lsq> ?m⇩V›
‹c⇩U ∈ X› ‹x ∈ disk(c⇩U,R⇩U)› ‹c⇩V ∈ X› ‹x ∈ disk(c⇩V,R⇩V)›
‹U = disk(c⇩U,R⇩U)› ‹V = disk(c⇩V,R⇩V)›
have "?W ⊆ U∩V" using disk_in_disk by blast
moreover from assms(2) ‹x∈X› ‹m ∈ L⇩+› have "?W ∈ B" and "x∈?W" using center_in_disk
by auto
ultimately show ?thesis by auto
qed
} then show ?thesis unfolding SatisfiesBaseCondition_def by auto
qed
text‹Disks centered at points farther away than the sum of radii do not overlap. ›
lemma (in pmetric_space) far_disks:
assumes "x∈X" "y∈X" "r⇩x\<ra>r⇩y \<lsq> d`⟨x,y⟩"
shows "disk(x,r⇩x)∩disk(y,r⇩y) = 0"
proof -
{ assume "disk(x,r⇩x)∩disk(y,r⇩y) ≠ 0"
then obtain z where "z ∈ disk(x,r⇩x)∩disk(y,r⇩y)" by auto
then have "z∈X" and "d`⟨x,z⟩ \<ra> d`⟨y,z⟩ \<ls> r⇩x\<ra>r⇩y"
using disk_definition add_ineq_strict by auto
moreover from assms(1,2) ‹z∈X› have "d`⟨x,y⟩ \<lsq> d`⟨x,z⟩ \<ra> d`⟨y,z⟩"
using pmetric_properties(3,4) by auto
ultimately have "d`⟨x,y⟩ \<ls> r⇩x\<ra>r⇩y" using loop_strict_ord_trans
by simp
with assms(3) have False using loop_strict_ord_trans by auto
} thus ?thesis by auto
qed
text‹ If we have a loop element that is smaller than the distance between two points, then
we can separate these points with disks.›
lemma (in pmetric_space) disjoint_disks:
assumes "x∈X" "y∈X" "r⇩x\<ls>d`⟨x,y⟩"
shows "(\<rm>r⇩x\<ad>(d`⟨x,y⟩)) ∈ L⇩+" and "disk(x,r⇩x)∩disk(y,\<rm>r⇩x\<ad>(d`⟨x,y⟩)) = 0"
proof -
from assms(3) show "(\<rm>r⇩x\<ad>(d`⟨x,y⟩)) ∈ L⇩+"
using ls_other_side posset_definition1 by simp
from assms(1,2,3) have "r⇩x∈L" and "d`⟨x,y⟩ ∈ L"
using less_members(1) pmetric_loop_valued(2) by auto
then have "r⇩x\<ra>(\<rm>r⇩x\<ad>(d`⟨x,y⟩)) = d`⟨x,y⟩" using lrdiv_props(6) by simp
with assms(1,2) ‹d`⟨x,y⟩ ∈ L› show "disk(x,r⇩x)∩disk(y,\<rm>r⇩x\<ad>(d`⟨x,y⟩)) = 0"
using loop_ord_refl far_disks by simp
qed
text‹Unions of disks form a topology, hence (pseudo)metric spaces are topological spaces. ›
theorem (in pmetric_space) pmetric_is_top:
assumes "r {down-directs} L⇩+"
defines "B ≡ ⋃c∈X. {disk(c,R). R∈L⇩+}"
defines "T ≡ {⋃A. A ∈ Pow(B)}"
shows "T {is a topology}" "B {is a base for} T" "⋃T = X"
proof -
from assms show "T {is a topology}" "B {is a base for} T"
using disks_form_base Top_1_2_T1 by auto
then have "⋃T = ⋃B" using Top_1_2_L5 by simp
moreover have "⋃B = X"
proof
from assms(2) show "⋃B ⊆ X" using disk_definition by auto
{ fix x assume "x∈X"
from assms(1) obtain R where "R∈L⇩+" unfolding DownDirects_def by blast
with assms(2) ‹x∈X› have "x ∈ ⋃B" using center_in_disk by auto
} thus "X ⊆ ⋃B" by auto
qed
ultimately show "⋃T = X" by simp
qed
text‹To define the ‹metric_space› locale we take the ‹pmetric_space› and add
the assumption of identity of indiscernibles.›
locale metric_space = pmetric_space +
assumes ident_indisc: "∀x∈X. ∀y∈X. d`⟨x,y⟩=𝟬 ⟶ x=y"
text‹In the ‹metric_space› locale $d$ is a metric.›
lemma (in metric_space) d_metric: shows "IsAmetric(d,X,L,A,r)"
using pmetricAssum ident_indisc unfolding IsAmetric_def by simp
text‹Distance of different points is greater than zero. ›
lemma (in metric_space) dist_pos: assumes "x∈X" "y∈X" "x≠y"
shows "𝟬\<ls>d`⟨x,y⟩" "d`⟨x,y⟩ ∈ L⇩+"
proof -
from assms(1,2) have "d`⟨x,y⟩ ∈ L⇧+"
using pmetric_properties(1) apply_funtype by simp
then have "𝟬 \<lsq> d`⟨x,y⟩" using Nonnegative_def by auto
with assms show "d`⟨x,y⟩ ∈ L⇩+" and "𝟬\<ls>d`⟨x,y⟩"
using ident_indisc posset_definition posset_definition1 by auto
qed
text‹An ordered loop valued metric space is $T_2$ (i.e. Hausdorff).›
theorem (in metric_space) metric_space_T2:
assumes "r {down-directs} L⇩+"
defines "B ≡ ⋃c∈X. {disk(c,R). R∈L⇩+}"
defines "T ≡ {⋃A. A ∈ Pow(B)}"
shows "T {is T⇩2}"
proof -
{ fix x y assume "x∈⋃T" "y∈⋃T" "x≠y"
from assms have "B⊆T" using pmetric_is_top(2) base_sets_open by auto
moreover have "∃U∈B. ∃V∈B. x∈U ∧ y∈V ∧ U∩V = 0"
proof -
let ?R = "d`⟨x,y⟩"
from assms have "⋃T = X" using pmetric_is_top(3) by simp
with ‹x∈⋃T› ‹y∈⋃T› have "x∈X" "y∈X" by auto
with ‹x≠y› have "?R∈L⇩+" using dist_pos by simp
with assms(2) ‹x∈X› ‹y∈X› have "disk(x,?R) ∈ B" and "disk(y,?R) ∈ B"
by auto
{ assume "disk(x,?R) ∩ disk(y,?R) = 0"
moreover from assms(2) ‹x∈X› ‹y∈X› ‹?R∈L⇩+› have
"disk(x,?R)∈B" "disk(y,?R)∈B" "x∈disk(x,?R)" "y∈disk(y,?R)"
using center_in_disk by auto
ultimately have "∃U∈B. ∃V∈B. x∈U ∧ y∈V ∧ U∩V = 0" by auto
}
moreover
{ assume "disk(x,?R) ∩ disk(y,?R) ≠ 0"
then obtain z where "z ∈ disk(x,?R)" and "z ∈ disk(y,?R)"
by auto
then have "d`⟨x,z⟩ \<ls> ?R" using disk_definition by simp
then have "𝟬 \<ls> \<rm>d`⟨x,z⟩\<ad>?R" using ls_other_side(1) by simp
let ?r = "\<rm>d`⟨x,z⟩\<ad>?R"
have "?r\<ls>?R"
proof -
from ‹z ∈ disk(y,?R)› ‹x∈X› ‹y∈X› have "z∈X" "x≠z"
using disk_definition pmetric_properties(3) by auto
with ‹x∈X› ‹y∈X› ‹z∈X› show ?thesis
using pmetric_loop_valued dist_pos(1) subtract_pos(2) by simp
qed
with ‹x∈X› ‹y∈X› have "disk(x,?r)∩disk(y,\<rm>?r\<ad>?R) = 0"
by (rule disjoint_disks)
moreover
from ‹𝟬\<ls>?r› ‹?r\<ls>?R› have "?r∈L⇩+" "(\<rm>?r\<ad>?R) ∈ L⇩+"
using ls_other_side posset_definition1 by auto
with assms(2) ‹x∈X› ‹y∈X› have
"disk(x,?r)∈B" "disk(y,\<rm>?r\<ad>(d`⟨x,y⟩))∈B" and
"x∈disk(x,?r)" "y∈disk(y,\<rm>?r\<ad>(d`⟨x,y⟩))"
using center_in_disk by auto
ultimately have "∃U∈B. ∃V∈B. x∈U ∧ y∈V ∧ U∩V = 0" by auto
}
ultimately show ?thesis by auto
qed
ultimately have "∃U∈T. ∃V∈T. x∈U ∧ y∈V ∧ U∩V = 0" by auto
} then show ?thesis unfolding isT2_def by simp
qed
end