fundamental system of entourages in a pseudometric space

IsarMathLib/MetricSpace_ZF.thy

@@ -28,7 +28,7 @@ EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)
 
 section \<open> Metric spaces \<close>
 
-theory MetricSpace_ZF imports Topology_ZF_1 OrderedLoop_ZF Lattice_ZF
+theory MetricSpace_ZF imports Topology_ZF_1 OrderedLoop_ZF Lattice_ZF UniformSpace_ZF
 begin
 
 text\<open>A metric space is a set on which a distance between points is defined as a function
@@ -147,11 +147,11 @@ proof
     using lrdiv_props(6) loop_strict_ord_trans disk_definition by simp
 qed
 
-text\<open> 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 
+text\<open> 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 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. \<close>
+  of the loop satisfies the base condition. The property that an order relation "down-directs"
+  a set is defined in \<open>Order_ZF\<close> and means that every two-element subset of the set 
+  has a lower bound in that set. \<close>
 
 lemma (in pmetric_space) disks_form_base: 
   assumes "r {down-directs} L\<^sub>+"
@@ -318,4 +318,159 @@ proof -
   } then show ?thesis unfolding isT2_def by simp
 qed
 
+subsection\<open>Uniform structures on metric spaces\<close>
+
+text\<open>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$.  \<close>
+
+text\<open>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$.\<close>
+
+definition
+  "UniformGauge(X,L,A,r,d) \<equiv> {d-``({b\<in>Nonnegative(L,A,r). \<langle>b,c\<rangle> \<in> r}). c\<in>PositiveSet(L,A,r)}"
+
+text\<open>In the \<open>pmetric_space\<close> context we will write \<open>UniformGauge(X,L,A,r,d)\<close> as \<open>\<BB>\<close>. \<close>
+
+abbreviation (in pmetric_space) gauge ("\<BB>") where "\<BB> \<equiv> UniformGauge(X,L,A,r,d)"
+
+text\<open>In notation defined in the \<open>pmetric_space\<close> context we can write the uniform gauge
+  as $\{d^{-1}(\{b\in L^+: b\leq c\} : c\in L_+\}$.  \<close>
+
+lemma (in pmetric_space) uniform_gauge_def_alt: 
+  shows "\<BB> = {d-``({c\<in>L\<^sup>+. c\<lsq>b}). b\<in>L\<^sub>+}"
+  unfolding UniformGauge_def by simp
+
+text\<open>If the distance between two points of $X$ is less or equal $b$, then
+  this pair of points is in $d^{-1}([0,b])$. \<close>
+
+lemma (in pmetric_space) gauge_members: 
+  assumes "x\<in>X" "y\<in>X" "d`\<langle>x,y\<rangle> \<lsq> b"
+  shows "\<langle>x,y\<rangle> \<in> d-``({c\<in>L\<^sup>+. c\<lsq>b})"
+  using assms pmetric_properties(1) apply_funtype func1_1_L15
+  by simp    
+
+text\<open>Gauges corresponding to larger elements of the loop are larger. \<close>
+
+lemma (in pmetric_space) uniform_gauge_mono: 
+  assumes "b\<^sub>1\<lsq>b\<^sub>2" shows "d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>1}) \<subseteq> d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>2})" 
+  using ordLoopAssum assms vimage_mono1 
+  unfolding IsAnOrdLoop_def IsPartOrder_def trans_def by auto
+
+text\<open>For any two sets of the form $d^{-1}([0,b])$ we can find a third one that is contained
+  in both. \<close>
+
+lemma (in pmetric_space) gauge_1st_cond: 
+  assumes "r {down-directs} L\<^sub>+" "B\<^sub>1\<in>\<BB>" "B\<^sub>2\<in>\<BB>"
+  shows "\<exists>B\<^sub>3\<in>\<BB>. B\<^sub>3\<subseteq>B\<^sub>1\<inter>B\<^sub>2" 
+proof -
+  from assms(2,3) obtain b\<^sub>1 b\<^sub>2 where "b\<^sub>1\<in>L\<^sub>+" "b\<^sub>2\<in>L\<^sub>+" and 
+    I: "B\<^sub>1 = d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>1})" "B\<^sub>2 = d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>2})"
+    using uniform_gauge_def_alt by auto
+  from assms(1) \<open>b\<^sub>1\<in>L\<^sub>+\<close> \<open>b\<^sub>2\<in>L\<^sub>+\<close> obtain b\<^sub>3 where "b\<^sub>3\<in>L\<^sub>+" "b\<^sub>3\<lsq>b\<^sub>1" "b\<^sub>3\<lsq>b\<^sub>2"
+    unfolding DownDirects_def by auto
+  from I \<open>b\<^sub>3\<lsq>b\<^sub>1\<close> \<open>b\<^sub>3\<lsq>b\<^sub>2\<close> have "d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>3}) \<subseteq> B\<^sub>1\<inter>B\<^sub>2"
+    using uniform_gauge_mono by blast
+  with \<open>b\<^sub>3\<in>L\<^sub>+\<close> show ?thesis using uniform_gauge_def_alt 
+    by auto
+qed
+
+text\<open>Sets of the form $d^{-1}([0,b])$ contain the diagonal. \<close>
+
+lemma (in pmetric_space) gauge_2nd_cond: assumes "B\<in>\<BB>" shows "id(X)\<subseteq>B"
+proof
+  fix p assume "p\<in>id(X)"
+  then obtain x where "x\<in>X" and "p=\<langle>x,x\<rangle>" by auto
+  then have "p\<in>X\<times>X" and "d`(p) = \<zero>" using pmetric_properties(2) by simp_all
+  from assms obtain b where "b\<in>L\<^sub>+" and "B = d-``({c\<in>L\<^sup>+. c\<lsq>b})"
+    using uniform_gauge_def_alt by auto
+  with \<open>p\<in>X\<times>X\<close> \<open>d`(p) = \<zero>\<close> show "p\<in>B"
+    using posset_definition1 loop_zero_nonneg pmetric_properties(1) func1_1_L15
+    by simp
+qed
+
+text\<open>Sets of the form $d^{-1}([0,b])$ are symmetric.\<close>
+
+lemma (in pmetric_space) gauge_symmetric: 
+  assumes "B\<in>\<BB>" shows "B = converse(B)"
+proof -
+  from assms obtain b where "B = d-``({c\<in>L\<^sup>+. 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\<open>A set of the form $d^{-1}([0,b])$ contains a symmetric set of this form.\<close>
+
+corollary (in pmetric_space) gauge_3rd_cond: 
+  assumes "B\<^sub>1\<in>\<BB>" shows "\<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 \<subseteq> converse(B\<^sub>1)"
+  using assms gauge_symmetric by auto
+
+text\<open>The sets of the form $d^{-1}([0,b])$ are subsets of $X\times X$. \<close>
+
+lemma (in pmetric_space) gauge_5thCond: shows "\<BB>\<subseteq>Pow(X\<times>X)"
+  using uniform_gauge_def_alt pmetric_properties(1) func1_1_L3 by force
+
+text\<open>If the set of positive values is non-empty, then there are sets
+  of the form $d^{-1}([0,b])$ for $b>0$.\<close>
+
+lemma (in pmetric_space) gauge_6thCond: 
+  assumes "L\<^sub>+\<noteq>\<emptyset>" shows "\<BB>\<noteq>\<emptyset>"  using assms uniform_gauge_def_alt by simp
+
+text\<open>The remaining 4th condition for the sets of the form $d^{-1}([0,b])$
+  to be a uniform base (fundamental system of entourages cannot be proven
+  without additional assumptions. 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 \<open>IsHalfable\<close>. \<close>
+
+definition
+  "IsHalfable(L,A,r) \<equiv> \<forall>b\<^sub>1\<in>PositiveSet(L,A,r). \<exists>b\<^sub>2\<in>PositiveSet(L,A,r). \<langle>A`\<langle>b\<^sub>2,b\<^sub>2\<rangle>,b\<^sub>1\<rangle> \<in> r"
+
+text\<open>The property of halfability written in the notation used in the \<open>pmetric_space\<close> context.\<close>
+
+lemma (in pmetric_space) is_halfable_def_alt: 
+  assumes "IsHalfable(L,A,r)" "b\<^sub>1\<in>L\<^sub>+"
+  shows "\<exists>b\<^sub>2\<in>L\<^sub>+. b\<^sub>2\<ra>b\<^sub>2 \<lsq> b\<^sub>1"
+  using assms unfolding IsHalfable_def by simp
+
+text\<open>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$.\<close>
+
+lemma (in pmetric_space) gauge_4thCond: 
+  assumes "IsHalfable(L,A,r)" "B\<^sub>1\<in>\<BB>" shows "\<exists>B\<^sub>2\<in>\<BB>.\<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 O B\<^sub>2 \<subseteq> B\<^sub>1"
+proof -
+  from assms(2) obtain b\<^sub>1 where "b\<^sub>1\<in>L\<^sub>+" and "B\<^sub>1 = d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>1})"
+    using uniform_gauge_def_alt by auto
+  from assms(1) \<open>b\<^sub>1\<in>L\<^sub>+\<close> obtain b\<^sub>2 where "b\<^sub>2\<in>L\<^sub>+" and "b\<^sub>2\<ra>b\<^sub>2 \<lsq> b\<^sub>1"
+    using is_halfable_def_alt by auto
+  let ?B\<^sub>2 = "d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>2})"
+  from \<open>b\<^sub>2\<in>L\<^sub>+\<close> have "?B\<^sub>2\<in>\<BB>" unfolding UniformGauge_def by auto
+  { fix p assume "p \<in> ?B\<^sub>2 O ?B\<^sub>2" 
+    with \<open>?B\<^sub>2\<in>\<BB>\<close> obtain x y where "x\<in>X" "y\<in>X" and "p=\<langle>x,y\<rangle>"
+      using gauge_5thCond by blast
+    from \<open>p \<in> ?B\<^sub>2 O ?B\<^sub>2\<close> \<open>p=\<langle>x,y\<rangle>\<close> obtain z where 
+      "\<langle>x,z\<rangle> \<in> ?B\<^sub>2" and "\<langle>z,y\<rangle> \<in> ?B\<^sub>2"
+      using rel_compdef by auto
+    with \<open>?B\<^sub>2\<in>\<BB>\<close> have "z\<in>X" using gauge_5thCond by auto
+    from \<open>\<langle>x,z\<rangle> \<in> ?B\<^sub>2\<close> \<open>\<langle>z,y\<rangle> \<in> ?B\<^sub>2\<close> have "d`\<langle>x,z\<rangle> \<ra> d`\<langle>z,y\<rangle> \<lsq> b\<^sub>2\<ra> b\<^sub>2"
+      using pmetric_properties(1) func1_1_L15 add_ineq by simp
+    with \<open>b\<^sub>2\<ra>b\<^sub>2 \<lsq> b\<^sub>1\<close> have "d`\<langle>x,z\<rangle> \<ra> d`\<langle>z,y\<rangle> \<lsq> b\<^sub>1"
+      using loop_ord_trans by simp
+    with \<open>x\<in>X\<close> \<open>y\<in>X\<close> \<open>z\<in>X\<close> \<open>p=\<langle>x,y\<rangle>\<close> \<open>B\<^sub>1 = d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>1})\<close> have "p\<in>B\<^sub>1"
+      using pmetric_properties(4) loop_ord_trans gauge_members by blast      
+  } hence "?B\<^sub>2 O ?B\<^sub>2 \<subseteq> B\<^sub>1" by auto
+  with \<open>?B\<^sub>2\<in>\<BB>\<close> show ?thesis by auto
+qed
+
+
 end

IsarMathLib/Order_ZF.thy

@@ -303,19 +303,19 @@ text\<open>Since there are some problems with applying the above lemma
   split \<open>Order_ZF_2_L1\<close> into two lemmas.\<close>
 
 lemma Order_ZF_2_L1A: assumes "x \<in> Interval(r,a,b)"
-  shows "\<langle> a,x\<rangle> \<in> r"  "\<langle> x,b\<rangle> \<in> r"
+  shows "\<langle>a,x\<rangle> \<in> r"  "\<langle>x,b\<rangle> \<in> r"
   using assms  Order_ZF_2_L1 by auto
 
 text\<open> \<open>Order_ZF_2_L1\<close>, implication from right to left.\<close>
 
-lemma Order_ZF_2_L1B: assumes "\<langle> a,x\<rangle> \<in> r"  "\<langle> x,b\<rangle> \<in> r"
+lemma Order_ZF_2_L1B: assumes "\<langle>a,x\<rangle> \<in> r"  "\<langle>x,b\<rangle> \<in> r"
   shows "x \<in> Interval(r,a,b)"
   using assms Order_ZF_2_L1 by simp
 
 text\<open>If the relation is reflexive, the endpoints belong to the interval.\<close>
 
 lemma Order_ZF_2_L2: assumes "refl(X,r)" 
-  and "a\<in>X"  "b\<in>X" and "\<langle> a,b\<rangle> \<in> r"
+  and "a\<in>X"  "b\<in>X" and "\<langle>a,b\<rangle> \<in> r"
   shows 
   "a \<in> Interval(r,a,b)"  
   "b \<in> Interval(r,a,b)"  
@@ -325,7 +325,7 @@ text\<open>Under the assumptions of \<open>Order_ZF_2_L2\<close>, the interval i
   nonempty.\<close>
 
 lemma Order_ZF_2_L2A: assumes "refl(X,r)" 
-  and "a\<in>X"  "b\<in>X" and "\<langle> a,b\<rangle> \<in> r"
+  and "a\<in>X"  "b\<in>X" and "\<langle>a,b\<rangle> \<in> r"
   shows "Interval(r,a,b) \<noteq> 0"
 proof -
   from assms have "a \<in> Interval(r,a,b)"
@@ -337,18 +337,18 @@ text\<open>If $a,b,c,d$ are in this order, then $[b,c]\subseteq [a,d]$. We
   only need trasitivity for this to be true.\<close>
 
 lemma Order_ZF_2_L3: 
-  assumes A1: "trans(r)" and A2:"\<langle> a,b\<rangle>\<in>r"  "\<langle> b,c\<rangle>\<in>r"  "\<langle> c,d\<rangle>\<in>r"
+  assumes A1: "trans(r)" and A2:"\<langle>a,b\<rangle>\<in>r"  "\<langle>b,c\<rangle>\<in>r"  "\<langle>c,d\<rangle>\<in>r"
 shows "Interval(r,b,c) \<subseteq> Interval(r,a,d)"
 proof
   fix x assume A3: "x \<in> Interval(r, b, c)"
   note A1
-  moreover from A2 A3 have "\<langle> a,b\<rangle> \<in> r \<and> \<langle> b,x\<rangle> \<in> r" using Order_ZF_2_L1A
+  moreover from A2 A3 have "\<langle>a,b\<rangle> \<in> r \<and> \<langle>b,x\<rangle> \<in> r" using Order_ZF_2_L1A
     by simp
-  ultimately have T1: "\<langle> a,x\<rangle> \<in> r" by (rule Fol1_L3)
+  ultimately have T1: "\<langle>a,x\<rangle> \<in> r" by (rule Fol1_L3)
   note A1
-  moreover from A2 A3 have "\<langle> x,c\<rangle> \<in> r \<and> \<langle> c,d\<rangle> \<in> r" using Order_ZF_2_L1A
+  moreover from A2 A3 have "\<langle>x,c\<rangle> \<in> r \<and> \<langle>c,d\<rangle> \<in> r" using Order_ZF_2_L1A
     by simp
-  ultimately have "\<langle> x,d\<rangle> \<in> r" by (rule Fol1_L3)
+  ultimately have "\<langle>x,d\<rangle> \<in> r" by (rule Fol1_L3)
   with T1 show "x \<in> Interval(r,a,d)" using Order_ZF_2_L1B
     by simp
 qed

IsarMathLib/OrderedLoop_ZF.thy

@@ -230,10 +230,17 @@ proof -
 qed
 
 text\<open> The loop order is reflexive. \<close>
+
 lemma (in loop1) loop_ord_refl: assumes "x\<in>L" shows "x\<lsq>x"
   using assms ordLoopAssum unfolding IsAnOrdLoop_def IsPartOrder_def refl_def 
   by simp
 
+text\<open>The neutral element is nonnegative.\<close>
+
+lemma (in loop1) loop_zero_nonneg: shows "\<zero>\<in>L\<^sup>+"
+  using neut_props_loop(1) loop_ord_refl nonneg_definition
+  by simp
+
 text\<open> A form of mixed transitivity for the strict order: \<close>
 
 lemma (in loop1) loop_strict_ord_trans: assumes "x\<lsq>y" and "y\<ls>z"

IsarMathLib/UniformSpace_ZF.thy

@@ -728,7 +728,7 @@ proof -
   ultimately show ?thesis unfolding IsUniformity_def by simp
 qed
 
-text\<open>The assumption that $X$ is empty in \<open>uniformity_base_is_base\<close> above is neccessary
+text\<open>The assumption that $X$ is not empty in \<open>uniformity_base_is_base\<close> above is neccessary
   as the assertion is false if $X$ is empty.\<close>
 
 lemma uniform_space_empty: assumes "\<BB> {is a uniform base on} \<emptyset>"

IsarMathLib/UniformSpace_ZF_2.thy

@@ -32,8 +32,8 @@ theory UniformSpace_ZF_2 imports UniformSpace_ZF
 begin
 
 text\<open> The \<open>UniformSpace_ZF\<close> theory defines uniform spaces based on entourages (also called surroundings 
-  sometimes). In this theory we consider an alternative definition based of the 
-  notion of uniform covers.
+  sometimes). In this theory we consider alternative definitions based of the 
+  notion of uniform covers and pseudometrics.
   \<close>
 
 subsection\<open> Uniform covers \<close>

IsarMathLib/func1.thy

@@ -231,7 +231,7 @@ text\<open>The inverse image of any set is contained in the domain.\<close>
 lemma func1_1_L6A: assumes A1: "f:X\<rightarrow>Y" shows "f-``(A)\<subseteq>X"
 proof
   fix x
-  assume A2: "x\<in>f-``(A)" then obtain y where "\<langle> x,y\<rangle> \<in> f" 
+  assume A2: "x\<in>f-``(A)" then obtain y where "\<langle>x,y\<rangle> \<in> f" 
     using vimage_iff by auto
   with A1 show  "x\<in>X" using func1_1_L5 by fast
 qed
@@ -241,6 +241,13 @@ text\<open>Image of a greater set is greater.\<close>
 lemma func1_1_L8: assumes A1: "A\<subseteq>B"  shows "f``(A)\<subseteq> f``(B)"
   using assms image_Un by auto
 
+text\<open>An immediate corollary of \<open>vimage_mono\<close> from the Isabelle/ZF distribution -
+  the inverse image of a greater set is greater. Note we do not require that
+  $f$ is a function, so this is true for relations as well.\<close>
+
+lemma vimage_mono1: assumes "A\<subseteq>B" shows "f-``(A) \<subseteq> f-``(B)"
+  using assms vimage_mono by simp
+
 text\<open>A set is contained in the the inverse image of its image.
   There is similar theorem in \<open>equalities.thy\<close>
   (\<open>function_image_vimage\<close>)
@@ -281,11 +288,10 @@ lemma func1_1_L11:
   assumes "f \<subseteq> X\<times>Y" and "\<forall>x\<in>X. \<exists>!y. y\<in>Y \<and> \<langle>x,y\<rangle> \<in> f"
   shows "f: X\<rightarrow>Y" using assms func1_1_L10 Pi_iff_old by simp
 
-text\<open>A set defined by a lambda-type expression is a fuction. There is a 
+text\<open>A set defined by a lambda-type expression is a function. There is a 
   similar lemma in func.thy, but I had problems with lambda expressions syntax
   so I could not apply it. This lemma is a workaround for this. Besides, lambda
-  expressions are not readable.
-\<close>
+  expressions are not readable. \<close>
 
 lemma func1_1_L11A: assumes A1: "\<forall>x\<in>X. b(x) \<in> Y"
   shows "{\<langle>x,y\<rangle> \<in> X\<times>Y. b(x) = y} : X\<rightarrow>Y"
@@ -635,6 +641,13 @@ proof -
   with A1 show ?thesis using func1_1_L14 by auto
 qed
 
+text\<open>For symmetric functions inverse images are symmetric.\<close>
+
+lemma symm_vimage_symm: 
+  assumes "f:X\<times>X\<rightarrow>Y" and "\<forall>x\<in>X. \<forall>y\<in>X. f`\<langle>x,y\<rangle> = f`\<langle>y,x\<rangle>"
+  shows "f-``(A) = converse(f-``(A))"
+  using assms func1_1_L15 by auto
+
 text\<open>A more familiar definition of image.\<close>
 
 lemma func_imagedef: assumes A1: "f:X\<rightarrow>Y" and A2: "A\<subseteq>X"
@@ -858,7 +871,7 @@ proof -
     by simp
 qed
 
-text\<open>What is the image of a set defined by a meta-fuction?\<close>
+text\<open>What is the image of a set defined by a meta-function?\<close>
 
 lemma func1_1_L17: 
   assumes A1: "f \<in> X\<rightarrow>Y" and A2: "\<forall>x\<in>A. b(x) \<in> X"