From e324059f78587de6e592cb1413cd47afdd3d7fe9 Mon Sep 17 00:00:00 2001 From: SKolodynski Date: Wed, 10 Jul 2024 20:34:16 +0200 Subject: [PATCH] fundamental system of entourages in a pseudometric space --- IsarMathLib/MetricSpace_ZF.thy | 165 +++++++++++++++++++++++++++++- IsarMathLib/Order_ZF.thy | 18 ++-- IsarMathLib/OrderedLoop_ZF.thy | 7 ++ IsarMathLib/UniformSpace_ZF.thy | 2 +- IsarMathLib/UniformSpace_ZF_2.thy | 4 +- IsarMathLib/func1.thy | 23 ++++- 6 files changed, 197 insertions(+), 22 deletions(-) diff --git a/IsarMathLib/MetricSpace_ZF.thy b/IsarMathLib/MetricSpace_ZF.thy index 6e01c34..4f16272 100644 --- a/IsarMathLib/MetricSpace_ZF.thy +++ b/IsarMathLib/MetricSpace_ZF.thy @@ -28,7 +28,7 @@ EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section \ Metric spaces \ -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\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\ 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\ 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. \ + 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\<^sub>+" @@ -318,4 +318,159 @@ proof - } 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}(\{b\in L^+: b\leq c\} : c\in L_+\}$. \ + +lemma (in pmetric_space) uniform_gauge_def_alt: + shows "\ = {d-``({c\L\<^sup>+. c\b}). b\L\<^sub>+}" + unfolding UniformGauge_def by simp + +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\ \ b" + shows "\x,y\ \ d-``({c\L\<^sup>+. c\b})" + using assms pmetric_properties(1) apply_funtype func1_1_L15 + by simp + +text\Gauges corresponding to larger elements of the loop are larger. \ + +lemma (in pmetric_space) uniform_gauge_mono: + assumes "b\<^sub>1\b\<^sub>2" shows "d-``({c\L\<^sup>+. c\b\<^sub>1}) \ d-``({c\L\<^sup>+. c\b\<^sub>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\<^sub>+" "B\<^sub>1\\" "B\<^sub>2\\" + shows "\B\<^sub>3\\. B\<^sub>3\B\<^sub>1\B\<^sub>2" +proof - + from assms(2,3) obtain b\<^sub>1 b\<^sub>2 where "b\<^sub>1\L\<^sub>+" "b\<^sub>2\L\<^sub>+" and + I: "B\<^sub>1 = d-``({c\L\<^sup>+. c\b\<^sub>1})" "B\<^sub>2 = d-``({c\L\<^sup>+. c\b\<^sub>2})" + using uniform_gauge_def_alt by auto + from assms(1) \b\<^sub>1\L\<^sub>+\ \b\<^sub>2\L\<^sub>+\ obtain b\<^sub>3 where "b\<^sub>3\L\<^sub>+" "b\<^sub>3\b\<^sub>1" "b\<^sub>3\b\<^sub>2" + unfolding DownDirects_def by auto + from I \b\<^sub>3\b\<^sub>1\ \b\<^sub>3\b\<^sub>2\ have "d-``({c\L\<^sup>+. c\b\<^sub>3}) \ B\<^sub>1\B\<^sub>2" + using uniform_gauge_mono by blast + with \b\<^sub>3\L\<^sub>+\ 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\<^sub>+" and "B = d-``({c\L\<^sup>+. c\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\<^sup>+. c\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\<^sub>1\\" shows "\B\<^sub>2\\. B\<^sub>2 \ converse(B\<^sub>1)" + using assms gauge_symmetric by auto + +text\The sets of the form $d^{-1}([0,b])$ are subsets 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\<^sub>+\\" 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 (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 \IsHalfable\. \ + +definition + "IsHalfable(L,A,r) \ \b\<^sub>1\PositiveSet(L,A,r). \b\<^sub>2\PositiveSet(L,A,r). \A`\b\<^sub>2,b\<^sub>2\,b\<^sub>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\<^sub>1\L\<^sub>+" + shows "\b\<^sub>2\L\<^sub>+. b\<^sub>2\b\<^sub>2 \ b\<^sub>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\<^sub>1\\" shows "\B\<^sub>2\\.\B\<^sub>2\\. B\<^sub>2 O B\<^sub>2 \ B\<^sub>1" +proof - + from assms(2) obtain b\<^sub>1 where "b\<^sub>1\L\<^sub>+" and "B\<^sub>1 = d-``({c\L\<^sup>+. c\b\<^sub>1})" + using uniform_gauge_def_alt by auto + from assms(1) \b\<^sub>1\L\<^sub>+\ obtain b\<^sub>2 where "b\<^sub>2\L\<^sub>+" and "b\<^sub>2\b\<^sub>2 \ b\<^sub>1" + using is_halfable_def_alt by auto + let ?B\<^sub>2 = "d-``({c\L\<^sup>+. c\b\<^sub>2})" + from \b\<^sub>2\L\<^sub>+\ have "?B\<^sub>2\\" unfolding UniformGauge_def by auto + { fix p assume "p \ ?B\<^sub>2 O ?B\<^sub>2" + with \?B\<^sub>2\\\ obtain x y where "x\X" "y\X" and "p=\x,y\" + using gauge_5thCond by blast + from \p \ ?B\<^sub>2 O ?B\<^sub>2\ \p=\x,y\\ obtain z where + "\x,z\ \ ?B\<^sub>2" and "\z,y\ \ ?B\<^sub>2" + using rel_compdef by auto + with \?B\<^sub>2\\\ have "z\X" using gauge_5thCond by auto + from \\x,z\ \ ?B\<^sub>2\ \\z,y\ \ ?B\<^sub>2\ have "d`\x,z\ \ d`\z,y\ \ b\<^sub>2\ b\<^sub>2" + using pmetric_properties(1) func1_1_L15 add_ineq by simp + with \b\<^sub>2\b\<^sub>2 \ b\<^sub>1\ have "d`\x,z\ \ d`\z,y\ \ b\<^sub>1" + using loop_ord_trans by simp + with \x\X\ \y\X\ \z\X\ \p=\x,y\\ \B\<^sub>1 = d-``({c\L\<^sup>+. c\b\<^sub>1})\ have "p\B\<^sub>1" + using pmetric_properties(4) loop_ord_trans gauge_members by blast + } hence "?B\<^sub>2 O ?B\<^sub>2 \ B\<^sub>1" by auto + with \?B\<^sub>2\\\ show ?thesis by auto +qed + + end diff --git a/IsarMathLib/Order_ZF.thy b/IsarMathLib/Order_ZF.thy index 868bb03..a8df120 100644 --- a/IsarMathLib/Order_ZF.thy +++ b/IsarMathLib/Order_ZF.thy @@ -303,19 +303,19 @@ text\Since there are some problems with applying the above lemma split \Order_ZF_2_L1\ into two lemmas.\ lemma Order_ZF_2_L1A: assumes "x \ Interval(r,a,b)" - shows "\ a,x\ \ r" "\ x,b\ \ r" + shows "\a,x\ \ r" "\x,b\ \ r" using assms Order_ZF_2_L1 by auto text\ \Order_ZF_2_L1\, implication from right to left.\ -lemma Order_ZF_2_L1B: assumes "\ a,x\ \ r" "\ x,b\ \ r" +lemma Order_ZF_2_L1B: assumes "\a,x\ \ r" "\x,b\ \ r" shows "x \ Interval(r,a,b)" using assms Order_ZF_2_L1 by simp text\If the relation is reflexive, the endpoints belong to the interval.\ lemma Order_ZF_2_L2: assumes "refl(X,r)" - and "a\X" "b\X" and "\ a,b\ \ r" + and "a\X" "b\X" and "\a,b\ \ r" shows "a \ Interval(r,a,b)" "b \ Interval(r,a,b)" @@ -325,7 +325,7 @@ text\Under the assumptions of \Order_ZF_2_L2\, the interval i nonempty.\ lemma Order_ZF_2_L2A: assumes "refl(X,r)" - and "a\X" "b\X" and "\ a,b\ \ r" + and "a\X" "b\X" and "\a,b\ \ r" shows "Interval(r,a,b) \ 0" proof - from assms have "a \ Interval(r,a,b)" @@ -337,18 +337,18 @@ text\If $a,b,c,d$ are in this order, then $[b,c]\subseteq [a,d]$. We only need trasitivity for this to be true.\ lemma Order_ZF_2_L3: - assumes A1: "trans(r)" and A2:"\ a,b\\r" "\ b,c\\r" "\ c,d\\r" + assumes A1: "trans(r)" and A2:"\a,b\\r" "\b,c\\r" "\c,d\\r" shows "Interval(r,b,c) \ Interval(r,a,d)" proof fix x assume A3: "x \ Interval(r, b, c)" note A1 - moreover from A2 A3 have "\ a,b\ \ r \ \ b,x\ \ r" using Order_ZF_2_L1A + moreover from A2 A3 have "\a,b\ \ r \ \b,x\ \ r" using Order_ZF_2_L1A by simp - ultimately have T1: "\ a,x\ \ r" by (rule Fol1_L3) + ultimately have T1: "\a,x\ \ r" by (rule Fol1_L3) note A1 - moreover from A2 A3 have "\ x,c\ \ r \ \ c,d\ \ r" using Order_ZF_2_L1A + moreover from A2 A3 have "\x,c\ \ r \ \c,d\ \ r" using Order_ZF_2_L1A by simp - ultimately have "\ x,d\ \ r" by (rule Fol1_L3) + ultimately have "\x,d\ \ r" by (rule Fol1_L3) with T1 show "x \ Interval(r,a,d)" using Order_ZF_2_L1B by simp qed diff --git a/IsarMathLib/OrderedLoop_ZF.thy b/IsarMathLib/OrderedLoop_ZF.thy index f67e7c5..7d37163 100644 --- a/IsarMathLib/OrderedLoop_ZF.thy +++ b/IsarMathLib/OrderedLoop_ZF.thy @@ -230,10 +230,17 @@ proof - qed text\ The loop order is reflexive. \ + lemma (in loop1) loop_ord_refl: assumes "x\L" shows "x\x" using assms ordLoopAssum unfolding IsAnOrdLoop_def IsPartOrder_def refl_def by simp +text\The neutral element is nonnegative.\ + +lemma (in loop1) loop_zero_nonneg: shows "\\L\<^sup>+" + using neut_props_loop(1) loop_ord_refl nonneg_definition + by simp + text\ A form of mixed transitivity for the strict order: \ lemma (in loop1) loop_strict_ord_trans: assumes "x\y" and "y\z" diff --git a/IsarMathLib/UniformSpace_ZF.thy b/IsarMathLib/UniformSpace_ZF.thy index db8a231..6585797 100644 --- a/IsarMathLib/UniformSpace_ZF.thy +++ b/IsarMathLib/UniformSpace_ZF.thy @@ -728,7 +728,7 @@ proof - ultimately show ?thesis unfolding IsUniformity_def by simp qed -text\The assumption that $X$ is empty in \uniformity_base_is_base\ above is neccessary +text\The assumption that $X$ is not empty in \uniformity_base_is_base\ above is neccessary as the assertion is false if $X$ is empty.\ lemma uniform_space_empty: assumes "\ {is a uniform base on} \" diff --git a/IsarMathLib/UniformSpace_ZF_2.thy b/IsarMathLib/UniformSpace_ZF_2.thy index 39a04b2..95722ee 100644 --- a/IsarMathLib/UniformSpace_ZF_2.thy +++ b/IsarMathLib/UniformSpace_ZF_2.thy @@ -32,8 +32,8 @@ theory UniformSpace_ZF_2 imports UniformSpace_ZF begin text\ The \UniformSpace_ZF\ 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. \ subsection\ Uniform covers \ diff --git a/IsarMathLib/func1.thy b/IsarMathLib/func1.thy index c0c5147..1d26621 100644 --- a/IsarMathLib/func1.thy +++ b/IsarMathLib/func1.thy @@ -231,7 +231,7 @@ text\The inverse image of any set is contained in the domain.\ lemma func1_1_L6A: assumes A1: "f:X\Y" shows "f-``(A)\X" proof fix x - assume A2: "x\f-``(A)" then obtain y where "\ x,y\ \ f" + assume A2: "x\f-``(A)" then obtain y where "\x,y\ \ f" using vimage_iff by auto with A1 show "x\X" using func1_1_L5 by fast qed @@ -241,6 +241,13 @@ text\Image of a greater set is greater.\ lemma func1_1_L8: assumes A1: "A\B" shows "f``(A)\ f``(B)" using assms image_Un by auto +text\An immediate corollary of \vimage_mono\ 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.\ + +lemma vimage_mono1: assumes "A\B" shows "f-``(A) \ f-``(B)" + using assms vimage_mono by simp + text\A set is contained in the the inverse image of its image. There is similar theorem in \equalities.thy\ (\function_image_vimage\) @@ -281,11 +288,10 @@ lemma func1_1_L11: assumes "f \ X\Y" and "\x\X. \!y. y\Y \ \x,y\ \ f" shows "f: X\Y" using assms func1_1_L10 Pi_iff_old by simp -text\A set defined by a lambda-type expression is a fuction. There is a +text\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. -\ + expressions are not readable. \ lemma func1_1_L11A: assumes A1: "\x\X. b(x) \ Y" shows "{\x,y\ \ X\Y. b(x) = y} : X\Y" @@ -635,6 +641,13 @@ proof - with A1 show ?thesis using func1_1_L14 by auto qed +text\For symmetric functions inverse images are symmetric.\ + +lemma symm_vimage_symm: + assumes "f:X\X\Y" and "\x\X. \y\X. f`\x,y\ = f`\y,x\" + shows "f-``(A) = converse(f-``(A))" + using assms func1_1_L15 by auto + text\A more familiar definition of image.\ lemma func_imagedef: assumes A1: "f:X\Y" and A2: "A\X" @@ -858,7 +871,7 @@ proof - by simp qed -text\What is the image of a set defined by a meta-fuction?\ +text\What is the image of a set defined by a meta-function?\ lemma func1_1_L17: assumes A1: "f \ X\Y" and A2: "\x\A. b(x) \ X"