Theory MetricSpace_ZF
section ‹ Metric spaces ›
theory MetricSpace_ZF imports Topology_ZF_1 OrderedLoop_ZF Lattice_ZF UniformSpace_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‹We define ‹metric topology› as consisting of unions of open disks.›
definition
"MetricTopology(X,L,A,r,d) ≡ {⋃𝒜. 𝒜 ∈ Pow(⋃c∈X. {Disk(X,d,r,c,R). R∈PositiveSet(L,A,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.
In the ‹pmetric_space› context $\tau$ denotes the topology defined by the metric $d$.
Analogously to the notation defined in the ‹topology0› context ‹int(A)›,
‹cl(A)›, ‹∂A› will denote the interior, closure and boundary of the set $A$
with respect to the metric topology. ›
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)"
fixes pmettop ("τ")
defines pmettop [simp]: "τ ≡ MetricTopology(X,L,A,r,d)"
fixes interior ("int")
defines interior_def [simp]: "int(D) ≡ Interior(D,τ)"
fixes cl
defines cl_def [simp]: "cl(D) ≡ Closure(D,τ)"
text‹ The next lemma shows the definition of the pseudometric in the notation used in the
‹pmetric_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 in the nonnegative set of the loop,
hence 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: if $c$ is an element
of $X$ and $x$ is in disk with center $c$ and radius $R$ then $R$ is a positive element of
$L$ and $-d(x,y)+R$ is in the set of positive elements of the loop. ›
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 -d\langle c,x\rangle + R$ 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‹A special case of ‹disk_in_disk› where we set $m = -d\langle c,x\rangle + R$:
if $x$ is an element of a disk with center $c\in X$
and radius $R$ then this disk contains the disk centered at $x$ and with radius
$-d\langle c,x\rangle + R$. ›
lemma (in pmetric_space) disk_in_disk1:
assumes "c∈X" and "x ∈ disk(c,R)"
shows "disk(x,\<rm>d`⟨c,x⟩ \<ad> R) ⊆ disk(c,R)"
proof -
from assms(2) have "R∈L" and "d`⟨c,x⟩ ∈ L"
using disk_definition less_members by auto
with assms show ?thesis using left_right_sub_closed(1) loop_ord_refl disk_in_disk
by simp
qed
text‹Assuming that two disks have the same center, closed disk with smaller radius
in contained in the (open) disk with a larger radius. ›
lemma (in pmetric_space) disk_radius_strict_mono:
assumes "r⇩1 \<ls> r⇩2"
shows "{y∈X. d`⟨x,y⟩ \<lsq> r⇩1} ⊆ disk(x,r⇩2)"
using assms loop_strict_ord_trans disk_definition by auto
text‹ If we assume that the loop's order relation down-directs $L_+$ then
the collection of disks centered at points of the space and with radii in the positive set
of the loop satisfies the base condition. The property that an order relation "down-directs"
a set is defined in ‹Order_ZF› and means that every two-element subset of the set
has a lower bound in that set. ›
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) = ∅"
proof -
{ assume "disk(x,r⇩x)∩disk(y,r⇩y) ≠ ∅"
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‹The definition of metric topology written in notation of ‹pmetric_space› context:›
lemma (in pmetric_space) metric_top_def_alt:
defines "B ≡ ⋃c∈X. {disk(c,R). R∈L⇩+}"
shows "τ = {⋃A. A ∈ Pow(B)}"
proof -
from assms have "MetricTopology(X,L,A,r,d) = {⋃A. A ∈ Pow(B)}"
unfolding MetricTopology_def by simp
thus ?thesis by simp
qed
text‹If the order of the loop down-directs its set of positive elements
then the metric topology defined as collection of unions of (open) disks is indeed a topology.
Recall that in the ‹pmetric_space› context $\tau$ denotes the metric topology. ›
theorem (in pmetric_space) pmetric_is_top:
assumes "r {down-directs} L⇩+"
shows "τ {is a topology}"
using assms disks_form_base Top_1_2_T1 metric_top_def_alt by simp
text‹If $r$ down-directs $L_+$ then the collection of open disks is a base for
the metric topology.›
theorem (in pmetric_space) disks_are_base:
assumes "r {down-directs} L⇩+"
defines "B ≡ ⋃c∈X. {disk(c,R). R∈L⇩+}"
shows "B {is a base for} τ"
using assms disks_form_base Top_1_2_T1 metric_top_def_alt by simp
text‹If $r$ down-directs $L_+$ then $X$ is the carrier of metric topology.›
theorem (in pmetric_space) metric_top_carrier:
assumes "r {down-directs} L⇩+" shows "⋃τ = X"
proof -
let ?B = "⋃c∈X. {disk(c,R). R∈L⇩+}"
from assms have "⋃τ = ⋃?B"
using disks_are_base Top_1_2_L5 by simp
moreover have "⋃?B = X"
proof
show "⋃?B ⊆ X" using disk_definition by auto
from assms show "X ⊆ ⋃?B" unfolding DownDirects_def using center_in_disk
by blast
qed
ultimately show "⋃τ = X" by simp
qed
text‹Under the assumption that $r$ down-directs $L_+$ the propositions proven
in the ‹topology0› context can be used in the ‹pmetric_space› context.›
lemma (in pmetric_space) topology0_valid_in_pmetric_space:
assumes "r {down-directs} L⇩+"
shows "topology0(τ)"
using assms pmetric_is_top unfolding topology0_def by simp
text‹If $r$ down-directs $L_+$ then disks are open in the metric topology.›
lemma (in pmetric_space) disks_open:
assumes "c∈X" "R∈L⇩+" "r {down-directs} L⇩+"
shows "disk(c,R) ∈ τ"
using assms base_sets_open disks_are_base(1) pmetric_is_top
by blast
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‹If $r$ down-directs $L_+$ then the ordered loop valued metric space is $T_2$ (i.e. Hausdorff).›
theorem (in metric_space) metric_space_T2:
assumes "r {down-directs} L⇩+"
shows "τ {is T⇩2}"
proof -
let ?B = "⋃c∈X. {disk(c,R). R∈L⇩+}"
{ fix x y assume "x∈⋃τ" "y∈⋃τ" "x≠y"
from assms have "?B⊆τ" using metric_top_def_alt by auto
have "∃U∈?B. ∃V∈?B. x∈U ∧ y∈V ∧ U∩V = ∅"
proof -
let ?R = "d`⟨x,y⟩"
from assms have "⋃τ = X" using metric_top_carrier by simp
with ‹x∈⋃τ› have "x∈X" by blast
from ‹⋃τ = X› ‹y∈⋃τ› have "y∈X" by blast
with ‹x≠y› ‹x∈X› have "?R∈L⇩+" using dist_pos by simp
with ‹x∈X› ‹y∈X› have "disk(x,?R) ∈ ?B" and "disk(y,?R) ∈ ?B"
by auto
{ assume "disk(x,?R) ∩ disk(y,?R) = ∅"
moreover from ‹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 blast
}
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) add_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 ‹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 blast
}
ultimately show ?thesis by auto
qed
with ‹?B⊆τ› have "∃U∈τ. ∃V∈τ. x∈U ∧ y∈V ∧ U∩V = ∅" by (rule exist2_subset)
} then show ?thesis unfolding isT2_def by simp
qed
subsection‹Uniform structures on metric spaces›
text‹Each pseudometric space with pseudometric $d:X\times X\rightarrow L$
supports a natural uniform structure, defined as supersets of the collection
of inverse images $U_c = d^{-1}([0,c])$, where $c>0$. ›
text‹In the following definition $X$ is the underlying space, $L$ is the loop (carrier),
$A$ is the loop operation, $r$ is an order relation compatible with $A$,
and $d$ is a pseudometric on $X$, valued in the ordered loop $L$.
With this we define the uniform gauge as the collection of inverse images
of the closed intervals $[0,c]$ as $c$ varies of the set of positive elements of $L$.›
definition
"UniformGauge(X,L,A,r,d) ≡ {d-``({b∈Nonnegative(L,A,r). ⟨b,c⟩ ∈ r}). c∈PositiveSet(L,A,r)}"
text‹In the ‹pmetric_space› context we will write ‹UniformGauge(X,L,A,r,d)› as ‹𝔅›. ›
abbreviation (in pmetric_space) gauge ("𝔅") where "𝔅 ≡ UniformGauge(X,L,A,r,d)"
text‹In notation defined in the ‹pmetric_space› context we can write the uniform gauge
as $\{ d^{-1}(\{c\in L^+: c\leq b\}: b \in L_+ \}$. ›
lemma (in pmetric_space) uniform_gauge_def_alt:
shows "𝔅 = {d-``({c∈L⇧+. c\<lsq>b}). b∈L⇩+}"
unfolding UniformGauge_def by simp
text‹Members of the uniform gauge are subsets of $X\times X$ i.e. relations on $X$. ›
lemma (in pmetric_space) uniform_gauge_relations:
assumes "B∈𝔅" shows "B⊆X×X"
using assms uniform_gauge_def_alt pmetric_properties(1) func1_1_L3
by force
text‹If the distance between two points of $X$ is less or equal $b$, then
this pair of points is in $d^{-1}([0,b])$. ›
lemma (in pmetric_space) gauge_members:
assumes "x∈X" "y∈X" "d`⟨x,y⟩ \<lsq> b"
shows "⟨x,y⟩ ∈ d-``({c∈L⇧+. c\<lsq>b})"
using assms pmetric_properties(1) apply_funtype func1_1_L15
by simp
text‹Suppose $b\in L^+$ (i.e. b is an element of the loop that is greater than the neutral element)
and $x\in X$. Then the image of the singleton set $\{ x\}$ by the relation
$B=\{ d^{-1}(\{c\in L^+: c\leq b\}$ is the set $\{ y\in X:d\langle x,y\rangle \leq b\}$,
i.e. the closed disk with center $x$ and radius $b$. Hence the the image $B\{ x\}$ contains
the open disk with center $x$ and radius $b$. ›
lemma (in pmetric_space) disk_in_gauge:
assumes "b∈L⇩+" "x∈X"
defines "B ≡ d-``({c∈L⇧+. c\<lsq>b})"
shows "B``{x} = {y∈X. d`⟨x,y⟩ \<lsq> b}" and "disk(x,b) ⊆ B``{x}"
proof -
from assms(1,3) have "B⊆X×X"
using uniform_gauge_def_alt uniform_gauge_relations by auto
with assms(2,3) show "B``{x} = {y∈X. d`⟨x,y⟩ \<lsq> b}"
using pmetric_properties(1) func1_1_L15 by force
then show "disk(x,b) ⊆ B``{x}" using disk_definition by auto
qed
text‹Gauges corresponding to larger elements of the loop are larger. ›
lemma (in pmetric_space) uniform_gauge_mono:
assumes "b⇩1\<lsq>b⇩2" shows "d-``({c∈L⇧+. c\<lsq>b⇩1}) ⊆ d-``({c∈L⇧+. c\<lsq>b⇩2})"
using ordLoopAssum assms vimage_mono1
unfolding IsAnOrdLoop_def IsPartOrder_def trans_def by auto
text‹For any two sets of the form $d^{-1}([0,b])$ we can find a third one that is contained
in both. ›
lemma (in pmetric_space) gauge_1st_cond:
assumes "r {down-directs} L⇩+" "B⇩1∈𝔅" "B⇩2∈𝔅"
shows "∃B⇩3∈𝔅. B⇩3⊆B⇩1∩B⇩2"
proof -
from assms(2,3) obtain b⇩1 b⇩2 where "b⇩1∈L⇩+" "b⇩2∈L⇩+" and
I: "B⇩1 = d-``({c∈L⇧+. c\<lsq>b⇩1})" "B⇩2 = d-``({c∈L⇧+. c\<lsq>b⇩2})"
using uniform_gauge_def_alt by auto
from assms(1) ‹b⇩1∈L⇩+› ‹b⇩2∈L⇩+› obtain b⇩3 where "b⇩3∈L⇩+" "b⇩3\<lsq>b⇩1" "b⇩3\<lsq>b⇩2"
unfolding DownDirects_def by auto
from I ‹b⇩3\<lsq>b⇩1› ‹b⇩3\<lsq>b⇩2› have "d-``({c∈L⇧+. c\<lsq>b⇩3}) ⊆ B⇩1∩B⇩2"
using uniform_gauge_mono by blast
with ‹b⇩3∈L⇩+› show ?thesis using uniform_gauge_def_alt
by auto
qed
text‹Sets of the form $d^{-1}([0,b])$ contain the diagonal. ›
lemma (in pmetric_space) gauge_2nd_cond: assumes "B∈𝔅" shows "id(X)⊆B"
proof
fix p assume "p∈id(X)"
then obtain x where "x∈X" and "p=⟨x,x⟩" by auto
then have "p∈X×X" and "d`(p) = 𝟬" using pmetric_properties(2) by simp_all
from assms obtain b where "b∈L⇩+" and "B = d-``({c∈L⇧+. c\<lsq>b})"
using uniform_gauge_def_alt by auto
with ‹p∈X×X› ‹d`(p) = 𝟬› show "p∈B"
using posset_definition1 loop_zero_nonneg pmetric_properties(1) func1_1_L15
by simp
qed
text‹Sets of the form $d^{-1}([0,b])$ are symmetric.›
lemma (in pmetric_space) gauge_symmetric:
assumes "B∈𝔅" shows "B = converse(B)"
proof -
from assms obtain b where "B = d-``({c∈L⇧+. c\<lsq>b})"
using uniform_gauge_def_alt by auto
with pmetricAssum show ?thesis unfolding IsApseudoMetric_def
using symm_vimage_symm by auto
qed
text‹A set of the form $d^{-1}([0,b])$ contains a symmetric set of this form.›
corollary (in pmetric_space) gauge_3rd_cond:
assumes "B⇩1∈𝔅" shows "∃B⇩2∈𝔅. B⇩2 ⊆ converse(B⇩1)"
using assms gauge_symmetric by auto
text‹The collection of sets of the form $d^{-1}([0,b])$ for $b\in L_+$
is contained of the powerset of $X\times X$.›
lemma (in pmetric_space) gauge_5thCond: shows "𝔅⊆Pow(X×X)"
using uniform_gauge_def_alt pmetric_properties(1) func1_1_L3 by force
text‹If the set of positive values is non-empty, then there are sets
of the form $d^{-1}([0,b])$ for $b>0$.›
lemma (in pmetric_space) gauge_6thCond:
assumes "L⇩+≠∅" shows "𝔅≠∅" using assms uniform_gauge_def_alt by simp
text‹The remaining 4th condition for the sets of the form $d^{-1}([0,b])$
to be a uniform base (or a fundamental system of entourages) cannot be proven
without additional assumptions in the context of ordered loop valued metrics.
To see that consider the example
of natural numbers with the metric $d\langle x,y \rangle = |x-y|$, where we think
of $d$ as valued in the nonnegative set of ordered group of integers.
Now take the set $B_1 = d^{-1}([0,1]) = d^{-1}(\{ 0,1\} )$. Then the set $B_1 \circ B_1$
is strictly larger than $B_1$, but there is no smaller set $B_2$ we can take so that
$B_2 \circ B_2 \subseteq B_1$.
One condition that is sufficient is that for every $b_1 >0$ there is a $b_2 >0$
such that $b_2 + b_2 \leq b_1 $. I have not found a standard name for this property, for now
we will use the name ‹IsHalfable›. ›
definition
"IsHalfable(L,A,r) ≡ ∀b⇩1∈PositiveSet(L,A,r). ∃b⇩2∈PositiveSet(L,A,r). ⟨A`⟨b⇩2,b⇩2⟩,b⇩1⟩ ∈ r"
text‹The property of halfability written in the notation used in the ‹pmetric_space› context.›
lemma (in pmetric_space) is_halfable_def_alt:
assumes "IsHalfable(L,A,r)" "b⇩1∈L⇩+"
shows "∃b⇩2∈L⇩+. b⇩2\<ra>b⇩2 \<lsq> b⇩1"
using assms unfolding IsHalfable_def by simp
text‹If the loop order is halfable then for every set $B_1$ of the form $d^{-1}([0,b_1])$
for some $b_1>0$ we can find another one $B_2 = d^{-1}([0,b_2])$ such that $B_2$
composed with itself is contained in $B_1$.›
lemma (in pmetric_space) gauge_4thCond:
assumes "IsHalfable(L,A,r)" "B⇩1∈𝔅" shows "∃B⇩2∈𝔅.∃B⇩2∈𝔅. B⇩2 O B⇩2 ⊆ B⇩1"
proof -
from assms(2) obtain b⇩1 where "b⇩1∈L⇩+" and "B⇩1 = d-``({c∈L⇧+. c\<lsq>b⇩1})"
using uniform_gauge_def_alt by auto
from assms(1) ‹b⇩1∈L⇩+› obtain b⇩2 where "b⇩2∈L⇩+" and "b⇩2\<ra>b⇩2 \<lsq> b⇩1"
using is_halfable_def_alt by auto
let ?B⇩2 = "d-``({c∈L⇧+. c\<lsq>b⇩2})"
from ‹b⇩2∈L⇩+› have "?B⇩2∈𝔅" unfolding UniformGauge_def by auto
{ fix p assume "p ∈ ?B⇩2 O ?B⇩2"
with ‹?B⇩2∈𝔅› obtain x y where "x∈X" "y∈X" and "p=⟨x,y⟩"
using gauge_5thCond by blast
from ‹p ∈ ?B⇩2 O ?B⇩2› ‹p=⟨x,y⟩› obtain z where
"⟨x,z⟩ ∈ ?B⇩2" and "⟨z,y⟩ ∈ ?B⇩2"
using rel_compdef by auto
with ‹?B⇩2∈𝔅› have "z∈X" using gauge_5thCond by auto
from ‹⟨x,z⟩ ∈ ?B⇩2› ‹⟨z,y⟩ ∈ ?B⇩2› have "d`⟨x,z⟩ \<ra> d`⟨z,y⟩ \<lsq> b⇩2\<ra> b⇩2"
using pmetric_properties(1) func1_1_L15 add_ineq by simp
with ‹b⇩2\<ra>b⇩2 \<lsq> b⇩1› have "d`⟨x,z⟩ \<ra> d`⟨z,y⟩ \<lsq> b⇩1"
using loop_ord_trans by simp
with ‹x∈X› ‹y∈X› ‹z∈X› ‹p=⟨x,y⟩› ‹B⇩1 = d-``({c∈L⇧+. c\<lsq>b⇩1})› have "p∈B⇩1"
using pmetric_properties(4) loop_ord_trans gauge_members by blast
} hence "?B⇩2 O ?B⇩2 ⊆ B⇩1" by auto
with ‹?B⇩2∈𝔅› show ?thesis by auto
qed
text‹If $X$ and $L_+$ are not empty, the order relation $r$
down-directs $L_+$, and the loop order is halfable, then $\mathfrak{B}$
(which in the ‹pmetric_space› context is an abbreviation for
$\{ d^{-1}(\{c\in L^+: c\leq b\}: b \in L_+ \}$)
is a fundamental system of entourages, hence its supersets
form a uniformity on $X$ and hence those supersets define a topology on $X$.›
theorem (in pmetric_space) metric_gauge_base:
assumes "X≠∅" "L⇩+≠∅" "r {down-directs} L⇩+" "IsHalfable(L,A,r)"
shows
"𝔅 {is a uniform base on} X"
"Supersets(X×X,𝔅) {is a uniformity on} X"
"UniformTopology(Supersets(X×X,𝔅),X) {is a topology}"
"⋃UniformTopology(Supersets(X×X,𝔅),X) = X"
using assms gauge_1st_cond gauge_2nd_cond gauge_3rd_cond
gauge_4thCond gauge_5thCond gauge_6thCond uniformity_base_is_base
uniform_top_is_top
unfolding IsUniformityBaseOn_def by simp_all
text‹At this point we know that a pseudometric induces two topologies: one consisting of unions
of open disks (the metric topology) and second one being the uniform topology derived
from the uniformity generated the fundamental system of entourages (the base uniformity)
of the sets of the form $d^{-1}([0,b])$ for $b>0$.
The next theorem states that if $X$ and $L_+$ are not empty, $r$ down-directs $L_+$,
and the loop order is halfable, then these two topologies are in fact the same.
Recall that in the ‹pmetric_space› context $\tau$ denotes the metric topology. ›
theorem (in pmetric_space) metric_top_is_uniform_top:
assumes "X≠∅" "L⇩+≠∅" "r {down-directs} L⇩+" "IsHalfable(L,A,r)"
shows "τ = UniformTopology(Supersets(X×X,𝔅),X)"
proof
let ?Φ = "Supersets(X×X,𝔅)"
from assms have "?Φ {is a uniformity on} X" using metric_gauge_base
by simp
let ?T = "UniformTopology(?Φ,X)"
{ fix U assume "U∈?T"
then have "U∈Pow(X)" and I: "∀x∈U. U∈{V``{x}. V∈?Φ}"
unfolding UniformTopology_def by auto
{ fix x assume "x∈U"
with I obtain A where "A∈?Φ" and "U = A``{x}"
by auto
from ‹x∈U› ‹U∈?T› have "x∈⋃?T" by auto
with assms have "x∈X" using metric_gauge_base(4) by simp
from ‹A∈?Φ› obtain B where "B∈𝔅" and "B⊆A"
unfolding Supersets_def by auto
from ‹B∈𝔅› obtain b where "b∈L⇩+" and "B = d-``({c∈L⇧+. c\<lsq>b})"
using uniform_gauge_def_alt by auto
with ‹x∈X› ‹B⊆A› ‹U = A``{x}› have "disk(x,b) ⊆ U"
using disk_in_gauge(2) by blast
with assms(3) ‹x∈X› ‹b∈L⇩+› have "∃V∈τ. x∈V ∧ V⊆U"
using disks_open center_in_disk by force
} with assms(3) have "U∈τ"
using topology0_valid_in_pmetric_space topology0.open_neigh_open
by simp
} thus "?T ⊆ τ" by auto
let ?𝒟 = "⋃c∈X. {disk(c,R). R∈L⇩+}"
{ fix U assume "U ∈ ?𝒟"
then obtain c b where "c∈X" "b∈L⇩+" "U = disk(c,b)"
by blast
{ fix x assume "x∈U"
let ?b⇩1 = "\<rm>d`⟨c,x⟩ \<ad> b"
from ‹x∈U› ‹c∈X› ‹U = disk(c,b)› have
"x∈X" "x∈disk(c,b)" "disk(x,?b⇩1) ⊆ U" "?b⇩1 ∈ L⇩+"
using disk_in_disk1 disk_definition radius_in_loop(4) by simp_all
with assms(4) obtain b⇩2 where "b⇩2∈L⇩+" and "b⇩2\<ra>b⇩2 \<lsq> ?b⇩1"
using is_halfable_def_alt by auto
let ?D = "{y∈X. d`⟨x,y⟩ \<lsq> b⇩2}"
from ‹b⇩2∈L⇩+› ‹b⇩2\<ra>b⇩2 \<lsq> ?b⇩1› have "?D ⊆ disk(x,?b⇩1)"
using posset_definition1 positive_subset add_subtract_pos(3)
loop_strict_ord_trans1 disk_radius_strict_mono by blast
let ?B = "d-``({c∈L⇧+. c\<lsq>b⇩2})"
from ‹b⇩2∈L⇩+› have "?B∈𝔅" using uniform_gauge_def_alt by auto
then have "?B∈?Φ" using uniform_gauge_relations superset_gen
by simp
from ‹b⇩2∈L⇩+› ‹x∈X› ‹?D ⊆ disk(x,?b⇩1)› ‹disk(x,?b⇩1) ⊆ U› have "?B``{x} ⊆ U"
using disk_in_gauge(1) by auto
with ‹?B∈?Φ› have "∃W∈?Φ. W``{x} ⊆ U" by auto
} with ‹U = disk(c,b)› ‹?Φ {is a uniformity on} X› have "U ∈ ?T"
using disk_definition uniftop_def_alt1 by auto
} hence "?𝒟 ⊆ ?T" by auto
with assms show "τ⊆?T"
using disks_are_base(1) metric_gauge_base(3) base_smallest_top
by simp
qed
end