(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2020,2021 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. *) 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