fundamental system of entourages for uniformity defined by family of pseudometrics

Author: SKolodynski

IsarMathLib/Finite_ZF.thy

@@ -452,16 +452,21 @@ proof -
   ultimately show "\<Union>N \<in> C" by (rule FinPow_induct)
 qed
 
-text\<open>Empty set is in finite power set.\<close>
+text\<open>Empty set is in finite power set, hence finite power set is never empty.\<close>
 
-lemma empty_in_finpow: shows "0 \<in> FinPow(X)"
-  using FinPow_def by simp
+lemma empty_in_finpow: shows "\<emptyset> \<in> FinPow(X)" and "FinPow(X)\<noteq>\<emptyset>"
+  using FinPow_def by auto
 
 text\<open>Singleton is in the finite powerset.\<close>
 
 lemma singleton_in_finpow: assumes "x \<in> X"
   shows "{x} \<in> FinPow(X)" using assms FinPow_def by simp
 
+text\<open>If a set is nonempty then its finite power set contains a nonempty set.\<close>
+
+lemma finpow_nempty_nempty: assumes "X\<noteq>\<emptyset>" shows "FinPow(X)\<setminus>{\<emptyset>} \<noteq> \<emptyset>"
+  using assms singleton_in_finpow by blast
+
 text\<open>Union of two finite subsets is a finite subset.\<close>
 
 lemma union_finpow: assumes "A \<in> FinPow(X)" and "B \<in> FinPow(X)"

IsarMathLib/MetricSpace_ZF.thy

@@ -596,34 +596,43 @@ lemma (in pmetric_space) is_halfable_def_alt:
   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 $B_i = d^{-1}(\{c \in L_+: c\leq b_i\})$ for $i=1,2$
+  and $b_2+b_2\leq b1$ then $B_2\circ B_2 \leq B_1$. The proof uses the triangle
+  inequality so it's not really a property of ordered loops only.\<close>
+
+lemma (in pmetric_space) half_vimage_square:
+  assumes "b\<^sub>2\<in>L\<^sub>+" and "b\<^sub>2\<ra>b\<^sub>2 \<lsq> b\<^sub>1"
+  defines "B\<^sub>1 \<equiv> d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>1})" and "B\<^sub>2 \<equiv> d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>2})"
+  shows "B\<^sub>2 O B\<^sub>2 \<subseteq> B\<^sub>1"
+proof
+  from assms(1,4) have "B\<^sub>2\<subseteq>X\<times>X" using pmetric_properties(1) func1_1_L3 by simp
+  fix p assume "p \<in> B\<^sub>2 O B\<^sub>2" 
+  with \<open>B\<^sub>2\<subseteq>X\<times>X\<close> obtain x y where "x\<in>X" "y\<in>X" and "p=\<langle>x,y\<rangle>"
+    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\<subseteq>X\<times>X\<close> have "z\<in>X" by auto
+  from assms(4) \<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 assms(3) \<open>x\<in>X\<close> \<open>y\<in>X\<close> \<open>z\<in>X\<close> \<open>p=\<langle>x,y\<rangle>\<close> show "p\<in>B\<^sub>1"
+    using pmetric_properties(4) loop_ord_trans gauge_members by blast
+qed
+
 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"
+  assumes "IsHalfable(L,A,r)" "B\<^sub>1\<in>\<BB>" shows "\<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
+  with \<open>B\<^sub>1 = d-``({c\<in>L\<^sup>+. c\<lsq>b\<^sub>1})\<close> show ?thesis 
+    using half_vimage_square unfolding UniformGauge_def by force
 qed
 
 text\<open>If $X$ and $L_+$ are not empty, the order relation $r$

IsarMathLib/MetricUniform_ZF.thy

@@ -97,9 +97,20 @@ text\<open>The next lemma just shows the definition of $\mathfrak{B}$ in notatio
   used in the \<open>muliple_pmetric\<close>. \<close>
 
 lemma (in muliple_pmetric) mgauge_def_alt: shows 
-  "UniformGaugeSets(X,L,A,r,M) = {(\<Inter>d\<in>M. d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)})). f\<in>M\<rightarrow>L\<^sub>+}"
   "\<BB> = (\<Union>M\<in>FinPow(\<M>)\<setminus>{\<emptyset>}. {(\<Inter>d\<in>M. d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)})). f\<in>M\<rightarrow>L\<^sub>+})"
-  unfolding UniformGaugeSets_def UniformGauges_def by simp_all
+  unfolding UniformGaugeSets_def UniformGauges_def by simp
+
+text\<open>$\mathfrak{B}$ consists of (finite) intersections of sets of the
+  form $d^{-1}(\{c\in L^+:c\leq f(d)\})$ where $f:M\rightarrow L_+$
+  some finite subset $M\subseteq \mathcal{M}$.
+  More precisely, if $M$ is a nonempty finite subset of $\mathcal{M}$ and $f$ maps 
+  $M$ to the positive set of the loop $L$, then the set 
+  $\bigcap_{d\in M} d^{-1}(\{c\in L^+:c\leq f(d)\}$ is in $\mathfrak{B}$.\<close>
+
+lemma (in muliple_pmetric) mgauge_finset_fun:
+  assumes "M\<in>FinPow(\<M>)" "M\<noteq>\<emptyset>" "f:M\<rightarrow>L\<^sub>+"
+  shows "(\<Inter>d\<in>M. d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)})) \<in> \<BB>"
+  using assms mgauge_def_alt by auto
 
 text\<open>If $d$ is one of the pseudometrics from $\mathcal{M}$ then theorems
   proven in \<open>pmetric_space\<close> can are valid. \<close>
@@ -157,7 +168,7 @@ proof -
   with I show "?L\<subseteq>?R" by (rule subset_trans)
 qed
 
-text\<open>For any two sets $B_1,B_2$ in $\mathcal{B}$ there exist a third one
+text\<open>For any two sets $B_1,B_2$ in $\mathfrak{B}$ there exist a third one
   that is contained in both. \<close>
 
 lemma (in muliple_pmetric) mgauge_1st_cond:
@@ -179,7 +190,7 @@ proof -
       by auto
   let ?B\<^sub>3 = "\<Inter>d\<in>?M\<^sub>3. d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>3`(d)})"
   from I(1,2) \<open>M\<^sub>1\<noteq>\<emptyset>\<close> \<open>f\<^sub>3:?M\<^sub>3\<rightarrow>L\<^sub>+\<close> have "?B\<^sub>3\<in>\<BB>"
-    using union_finpow mgauge_def_alt(2) by auto
+    using union_finpow mgauge_def_alt by auto
   moreover have "?B\<^sub>3\<subseteq>B\<^sub>1\<inter>B\<^sub>2"
   proof - 
     from I(1,2) have "M\<^sub>1\<subseteq>\<M>" "M\<^sub>1\<subseteq>?M\<^sub>3" "M\<^sub>2\<subseteq>\<M>" "M\<^sub>2\<subseteq>?M\<^sub>3"
@@ -190,5 +201,72 @@ proof -
   qed
   ultimately show "\<exists>B\<in>\<BB>. B\<subseteq>B\<^sub>1\<inter>B\<^sub>2" by (rule witness_exists)
 qed
-  
+
+text\<open>Sets in $\mathfrak{B}$ contain the diagonal and are symmetric,
+  hence contain a symmetric subset from $\mathfrak{B}$.\<close>
+
+lemma (in muliple_pmetric) mgauge_2nd_and_3rd_cond: assumes "B\<in>\<BB>" 
+  shows "id(X)\<subseteq>B" "B = converse(B)" "\<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 \<subseteq> converse(B)" 
+proof -
+  from assms obtain M f where "M\<in>FinPow(\<M>)" "M\<noteq>\<emptyset>" "f:M\<rightarrow>L\<^sub>+" and
+    I: "B = (\<Inter>d\<in>M. d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)}))"
+    using mgauge_def_alt by auto
+  { fix d assume "d\<in>M"
+    let ?B\<^sub>d = "d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)})"
+    from \<open>d\<in>M\<close> \<open>f:M\<rightarrow>L\<^sub>+\<close> \<open>M\<in>FinPow(\<M>)\<close> have
+      "pmetric_space(L,A,r,d,X)" and "?B\<^sub>d \<in> UniformGauge(X,L,A,r,d)"
+      unfolding FinPow_def UniformGauge_def 
+      using apply_funtype pmetric_space_valid_in_mpm by auto
+    then have "id(X)\<subseteq>?B\<^sub>d" and "?B\<^sub>d = converse(?B\<^sub>d)" 
+      using pmetric_space.gauge_2nd_cond pmetric_space.gauge_symmetric 
+      by simp_all
+  } with I \<open>M\<noteq>\<emptyset>\<close> show "id(X)\<subseteq>B" and "B = converse(B)" by auto
+  from assms \<open>B = converse(B)\<close> show "\<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 \<subseteq> converse(B)"
+    by auto
+qed
+
+text\<open>$\mathfrak{B}$ is a subset of the power set of $X\times X$.\<close>
+
+lemma (in muliple_pmetric) mgauge_5thCond: shows "\<BB>\<subseteq>Pow(X\<times>X)"
+  using muniform_gauge_relations by auto
+
+text\<open>If $\mathcal{M}$ and $L_+$ are nonempty then $\mathfrak{B}$ is also nonempty.\<close>
+
+lemma (in muliple_pmetric) mgauge_6thCond:
+  assumes "\<M>\<noteq>\<emptyset>" and "L\<^sub>+\<noteq>\<emptyset>" shows "\<BB>\<noteq>\<emptyset>" 
+proof -
+  from assms obtain M y where "M\<in>FinPow(\<M>)" "M\<noteq>\<emptyset>" and "y\<in>L\<^sub>+"
+    using finpow_nempty_nempty by blast
+  from \<open>y\<in>L\<^sub>+\<close> have "ConstantFunction(M,y):M\<rightarrow>L\<^sub>+" using func1_3_L1 by simp
+  with \<open>M\<in>FinPow(\<M>)\<close> \<open>M\<noteq>\<emptyset>\<close> show "\<BB>\<noteq>\<emptyset>" using mgauge_finset_fun by auto
+qed
+
+text\<open>If the loop order is halfable then for every set $B_1\in \mathfrak{B}$
+  there is another set $B_2\in \mathfrak{B}$ such that $B_2\circ B_2 \subseteq B_1$.\<close>
+
+lemma (in muliple_pmetric) mgauge_4thCond: 
+  assumes "IsHalfable(L,A,r)" "B\<^sub>1\<in>\<BB>" shows "\<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 O B\<^sub>2 \<subseteq> B\<^sub>1"
+proof -
+  from assms(2) obtain M f\<^sub>1 where "M\<in>FinPow(\<M>)" "M\<noteq>\<emptyset>" "f\<^sub>1:M\<rightarrow>L\<^sub>+" and
+    I: "B\<^sub>1 = (\<Inter>d\<in>M. d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>1`(d)}))"
+    using mgauge_def_alt by auto
+  from assms(1) \<open>f\<^sub>1:M\<rightarrow>L\<^sub>+\<close> have "\<forall>d\<in>M. \<exists>b\<^sub>2\<in>L\<^sub>+. b\<^sub>2\<ra>b\<^sub>2 \<lsq> f\<^sub>1`(d)"
+    using apply_funtype unfolding IsHalfable_def by simp
+  with \<open>M\<in>FinPow(\<M>)\<close> have "\<exists>f\<^sub>2\<in>M\<rightarrow>L\<^sub>+. \<forall>d\<in>M. f\<^sub>2`(d) \<ra> f\<^sub>2`(d) \<lsq> f\<^sub>1`(d)"
+    unfolding FinPow_def using finite_choice_fun by auto
+  then obtain f\<^sub>2 where "f\<^sub>2\<in>M\<rightarrow>L\<^sub>+" and II: "\<forall>d\<in>M. f\<^sub>2`(d) \<ra> f\<^sub>2`(d) \<lsq> f\<^sub>1`(d)"
+    by auto
+  let ?B\<^sub>2 = "\<Inter>d\<in>M. d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>2`(d)})" 
+  { fix d assume "d\<in>M"
+    let ?A\<^sub>2 = "d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>2`(d)})"
+    from \<open>d\<in>M\<close> \<open>M\<in>FinPow(\<M>)\<close> have "pmetric_space(L,A,r,d,X)"
+      unfolding FinPow_def using pmetric_space_valid_in_mpm by auto 
+    with \<open>f\<^sub>2\<in>M\<rightarrow>L\<^sub>+\<close> \<open>d\<in>M\<close> II have "?A\<^sub>2 O ?A\<^sub>2 \<subseteq> d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>1`(d)})"
+      using apply_funtype pmetric_space.half_vimage_square by simp
+  } 
+  with \<open>M\<noteq>\<emptyset>\<close> I have "?B\<^sub>2 O ?B\<^sub>2 \<subseteq> B\<^sub>1" using square_incl_product by simp
+  with \<open>M\<in>FinPow(\<M>)\<close> \<open>M\<noteq>\<emptyset>\<close> \<open>f\<^sub>2\<in>M\<rightarrow>L\<^sub>+\<close> show ?thesis
+    using mgauge_finset_fun by auto
+qed
+     
 end

IsarMathLib/ZF1.thy

@@ -476,6 +476,17 @@ proof -
   with assms(1) \<open>\<langle>x,t\<rangle> \<in> R O W\<close> show ?thesis by auto
 qed
 
+text\<open>Suppose we have two families of sets $\{ A(i)\}_{i\in I}$
+  and $\{ B(i)\}_{i\in I}$, indexed by a nonepty set of indices $I$
+  and such that for every index $i\in I$ we have inclusion
+  $A(i)\circ A(i) \subseteq B(i)$. Then a similar inclusion holds
+  for the products of the families, namely 
+  $(\bigcap_{i\in I}A(i))\circ (\bigcap_{i\in I}A(i)) \subseteq (\bigcap_{i\in I}B(i)$.\<close>
+
+lemma square_incl_product: assumes "I\<noteq>\<emptyset>" "\<forall>i\<in>I. A(i) O A(i) \<subseteq> B(i)"
+  shows "(\<Inter>i\<in>I. A(i)) O (\<Inter>i\<in>I. A(i)) \<subseteq> (\<Inter>i\<in>I. B(i))"
+  using assms by force
+
 text\<open> It's hard to believe but there are cases where we have to reference this rule. \<close>
 
 lemma set_mem_eq: assumes "x\<in>A" "A=B" shows "x\<in>B" using assms by simp