1+ (*
2+ This file is a part of IsarMathLib -
3+ a library of formalized mathematics for Isabelle/Isar.
4+
5+ Copyright (C) 2025 Slawomir Kolodynski
6+
7+ This program is free software; Redistribution and use in source and binary forms,
8+ with or without modification, are permitted provided that the following conditions are met:
9+
10+ 1. Redistributions of source code must retain the above copyright notice,
11+ this list of conditions and the following disclaimer.
12+ 2. Redistributions in binary form must reproduce the above copyright notice,
13+ this list of conditions and the following disclaimer in the documentation and/or
14+ other materials provided with the distribution.
15+ 3. The name of the author may not be used to endorse or promote products
16+ derived from this software without specific prior written permission.
17+
18+ THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED
19+ WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
20+ MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
21+ IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
22+ SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
23+ PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
24+ OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
25+ WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
26+ OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
27+ EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28+
29+ *)
30+
31+ section \<open>Uniformity defined by a a collection of pseudometrics\<close>
32+
33+ theory MetricUniform_ZF imports FinOrd_ZF_1 MetricSpace_ZF
34+
35+ begin
36+
37+ text \<open>In the \<open>MetricSpace_ZF\<close> we show how a single ( ordered loop valued ) pseudometric
38+ defines a uniformity. In this theory we extend this to the situation where we have
39+ an arbitrary collection of pseudometrics , all defined on the the same set $X $ and valued
40+ in an ordered loop $L $. Since real numbers form an ordered loop all the results proven in
41+ this theory are true for the standard real - valued pseudometrics. \<close>
42+
43+ subsection \<open>Definitions and notation\<close>
44+
45+ text \<open>Suppose $\mathcal{M}$ is a collection of (an ordered loop valued) pseudometrics on $X$,
46+ i.e. $d:X\times X\rightarrow L^+$ is a pseudometric for every $d\in \mathcal{M}$.
47+ Then, for each $d\in \mathcal{M}$ the sets $\{ d^{-1}(\{c\in L^+: c\leq b\}): b \in L_+ \}$
48+ form a fundamental system of entourages (see \<open>MetricSpace_ZF\<close> ) . \<close>
49+
50+ text \<open>The next two definitions describe the way a common fundamental system of entourages
51+ for $\mathcal{M}$ is constructed. First we take finite subset $M$ of $\mathcal{M}$.
52+ Then we choose $f:M\rightarrow L_+$. This way for each $d\in M$
53+ the value $f(d)$ is a positive element of $L$ and
54+ $\{d^{-1}(\{c\in L^+: c\leq f(d)\}): d\in M\}$ is a finite collection of
55+ subsets of $X\times X$. Then we take intersections of such finite
56+ collections as $M$ varies over $\mathcal{M}$ and $f$ varies over all possible function mapping
57+ $M$ to $L_+$. To simplify notation for this construction we split it into two steps.
58+ In the first step we define a collection of finite intersections resulting from
59+ choosing a finite set of pseudometrics $M$, $f:M\rightarrow L_+$ and varying
60+ the selector function $f$ over the space of functions mapping $M$ to the set of
61+ positive elements of $L$. \<close>
62+
63+ definition
64+ "UniformGaugeSets(X,L,A,r,M) \<equiv>
65+ {(\<Inter>d\<in>M. d-``({c\<in>Nonnegative(L,A,r). \<langle>c,f`(d)\<rangle> \<in> r})). f\<in>M\<rightarrow>PositiveSet(L,A,r)}"
66+
67+ text \<open>In the second step we collect all uniform gauge sets defined above
68+ as parameter $M$ vary over all nonempty finite subsets of $\mathcal{M}$.
69+ This is the collection of sets that we will show forms a fundamental system of entourages.\<close>
70+
71+ definition
72+ "UniformGauges(X,L,A,r,\<M>) \<equiv> \<Union>M\<in>FinPow(\<M>)\<setminus>{\<emptyset>}. UniformGaugeSets(X,L,A,r,M)"
73+
74+ text \<open>The context \<open>muliple_pmetric\<close> is very similar to the \<open>pmetric_space\<close> context
75+ except that rather than fixing a single pseudometric $d $ we fix a
76+ collection of pseudometrics $\mathcal { M } $. That forces the notation for
77+ \<open>disk\<close> , topology , interior and closure to depend on the pseudometric $d $. \<close>
78+
79+ locale muliple_pmetric = loop1 +
80+ fixes \<M> and X
81+ assumes mpmetricAssm : "\<forall>d\<in>\<M>. IsApseudoMetric(d,X,L,A,r)"
82+ fixes disk
83+ defines disk_def [ simp ]: "disk(d,c,R) \<equiv> Disk(X,d,r,c,R)"
84+ fixes pmettop ( "\<tau>" )
85+ defines pmettop [ simp ]: "\<tau>(d) \<equiv> MetricTopology(X,L,A,r,d)"
86+ fixes interior ( "int" )
87+ defines interior_def [ simp ]: "int(d,D) \<equiv> Interior(D,\<tau>(d))"
88+ fixes cl
89+ defines cl_def [ simp ]: "cl(d,D) \<equiv> Closure(D,\<tau>(d))"
90+
91+ text \<open>Analogously what is done in the \<open>pmetric_space\<close> context
92+ we will write \<open>UniformGauges(X,L,A,r,\<M>)\<close> as \<open>\<BB>\<close> in the \<open>muliple_pmetric\<close> context . \<close>
93+
94+ abbreviation ( in muliple_pmetric ) mgauge ( "\<BB>" ) where "\<BB> \<equiv> UniformGauges(X,L,A,r,\<M>)"
95+
96+ text \<open>The next lemma just shows the definition of $\mathfrak{B}$ in notation
97+ used in the \<open>muliple_pmetric\<close> . \<close>
98+
99+ lemma ( in muliple_pmetric ) mgauge_def_alt : shows
100+ "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>+}"
101+ "\<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>+})"
102+ unfolding UniformGaugeSets_def UniformGauges_def by simp_all
103+
104+ text \<open>If $d$ is one of the pseudometrics from $\mathcal{M}$ then theorems
105+ proven in \<open>pmetric_space\<close> can are valid. \<close>
106+
107+ lemma ( in muliple_pmetric ) pmetric_space_valid_in_mpm :
108+ assumes "d\<in>\<M>" shows "pmetric_space(L,A,r,d,X)"
109+ proof
110+ from assms mpmetricAssm show "IsApseudoMetric(d,X,L,A,r)" by simp
111+ qed
112+
113+ text \<open>If $d$ is member of any finite subset of $\mathcal{M}$ then
114+ $d$ maps $X\times X$ to the nonnegative set of the ordered loop $L$.\<close>
115+
116+ lemma ( in muliple_pmetric ) each_pmetric_map :
117+ assumes "M\<in>FinPow(\<M>)" and "d\<in>M" shows "d: X\<times>X \<rightarrow> L\<^sup>+"
118+ using assms pmetric_space_valid_in_mpm pmetric_space.pmetric_properties ( 1 )
119+ unfolding FinPow_def by auto
120+
121+ text \<open>Members of the uniform gauge defined by multiple pseudometrics
122+ are subsets of $X\times X$ i.e. relations on $X$. \<close>
123+
124+ lemma ( in muliple_pmetric ) muniform_gauge_relations :
125+ assumes "B\<in>\<BB>" shows "B\<subseteq>X\<times>X"
126+ proof -
127+ from assms obtain M f where "M\<in>FinPow(\<M>)" and
128+ I : "B = (\<Inter>d\<in>M. d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)}))"
129+ using mgauge_def_alt by auto
130+ { fix d assume "d\<in>M"
131+ with \<open>M\<in>FinPow(\<M>)\<close> have "d: X\<times>X \<rightarrow> L\<^sup>+"
132+ using each_pmetric_map by simp
133+ then have "d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)}) \<subseteq> X\<times>X" using func1_1_L15 by auto
134+ } with I show ?thesis using inter_subsets_subset by simp
135+ qed
136+
137+ text \<open>Suppose $M_1$ is a subset of $M$ and $\mathcal{M}$.
138+ $f_1,f$ map $M_1$ and $M$, resp. to $L_+$ and $f\leq f_1$ on $M_1$.
139+ Then the set $\bigcap_{d\in M} d^{-1}(\{y \in L_+: y\leq f(d)\})$
140+ is included in the set $\bigcap_{d\in M_1} d^{-1}(\{y \in L_+: y\leq f_1(d)\})$. \<close>
141+
142+ lemma ( in muliple_pmetric ) fun_inter_vimage_mono :
143+ assumes "M\<^sub>1\<subseteq>\<M>" "M\<^sub>1\<subseteq>M" "M\<^sub>1\<noteq>\<emptyset>" "f\<^sub>1:M\<^sub>1\<rightarrow>L\<^sub>+" "f:M\<rightarrow>L\<^sub>+" and
144+ "\<forall>d\<in>M\<^sub>1. f`(d)\<lsq>f\<^sub>1`(d)"
145+ shows
146+ "(\<Inter>d\<in>M. d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)})) \<subseteq> (\<Inter>d\<in>M\<^sub>1. d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>1`(d)}))"
147+ proof -
148+ let ?L = "(\<Inter>d\<in>M. d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)}))"
149+ let ?R = "(\<Inter>d\<in>M\<^sub>1. d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>1`(d)}))"
150+ from assms ( 2 , 3 ) have I : "?L \<subseteq> (\<Inter>d\<in>M\<^sub>1. d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)}))"
151+ using inter_index_mono by simp
152+ from assms ( 1 , 6 ) have
153+ "\<forall>d\<in>M\<^sub>1. (d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)})) \<subseteq> d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>1`(d)})"
154+ using pmetric_space_valid_in_mpm pmetric_space.uniform_gauge_mono
155+ by force
156+ with assms ( 2 ) have "(\<Inter>d\<in>M\<^sub>1. d-``({c\<in>L\<^sup>+. c\<lsq>f`(d)})) \<subseteq> ?R" by force
157+ with I show "?L\<subseteq>?R" by ( rule subset_trans )
158+ qed
159+
160+ text \<open>For any two sets $B_1,B_2$ in $\mathcal{B}$ there exist a third one
161+ that is contained in both. \<close>
162+
163+ lemma ( in muliple_pmetric ) mgauge_1st_cond :
164+ assumes "r {down-directs} L\<^sub>+" "B\<^sub>1\<in>\<BB>" "B\<^sub>2\<in>\<BB>"
165+ shows "\<exists>B\<in>\<BB>. B\<subseteq>B\<^sub>1\<inter>B\<^sub>2"
166+ proof -
167+ from assms ( 2 , 3 ) obtain M \<^sub >1 f \<^sub >1 M \<^sub >2 f \<^sub >2 where "M\<^sub>1\<noteq>\<emptyset>" "M\<^sub>2\<noteq>\<emptyset>" and
168+ I : "M\<^sub>1\<in>FinPow(\<M>)" "M\<^sub>2\<in>FinPow(\<M>)" "f\<^sub>1:M\<^sub>1\<rightarrow>L\<^sub>+" "f\<^sub>2:M\<^sub>2\<rightarrow>L\<^sub>+" and
169+ II : "B\<^sub>1 = (\<Inter>d\<in>M\<^sub>1. d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>1`(d)}))" "B\<^sub>2 = (\<Inter>d\<in>M\<^sub>2. d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>2`(d)}))"
170+ using mgauge_def_alt by auto
171+ let ?M \<^sub >3 = "M\<^sub>1\<union>M\<^sub>2"
172+ from assms ( 1 ) have "IsDownDirectedSet(L\<^sub>+,r)" using down_directs_directed
173+ by simp
174+ with I have
175+ "\<exists>f\<^sub>3\<in>?M\<^sub>3\<rightarrow>L\<^sub>+. (\<forall>d\<in>M\<^sub>1. \<langle>f\<^sub>3`(d),f\<^sub>1`(d)\<rangle>\<in>r) \<and> (\<forall>d\<in>M\<^sub>2. \<langle>f\<^sub>3`(d),f\<^sub>2`(d)\<rangle>\<in>r)"
176+ using two_fun_low_bound by simp
177+ then obtain f \<^sub >3 where "f\<^sub>3:?M\<^sub>3\<rightarrow>L\<^sub>+" and
178+ III : "\<forall>d\<in>M\<^sub>1. f\<^sub>3`(d)\<lsq>f\<^sub>1`(d)" "\<forall>d\<in>M\<^sub>2. f\<^sub>3`(d)\<lsq>f\<^sub>2`(d)"
179+ by auto
180+ let ?B \<^sub >3 = "\<Inter>d\<in>?M\<^sub>3. d-``({c\<in>L\<^sup>+. c\<lsq>f\<^sub>3`(d)})"
181+ 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>"
182+ using union_finpow mgauge_def_alt ( 2 ) by auto
183+ moreover have "?B\<^sub>3\<subseteq>B\<^sub>1\<inter>B\<^sub>2"
184+ proof -
185+ 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"
186+ unfolding FinPow_def by auto
187+ with \<open>M\<^sub>1\<noteq>\<emptyset>\<close> \<open>M\<^sub>2\<noteq>\<emptyset>\<close> I ( 3 , 4 ) II \<open>f\<^sub>3:?M\<^sub>3\<rightarrow>L\<^sub>+\<close> III
188+ have "?B\<^sub>3\<subseteq>B\<^sub>1" and "?B\<^sub>3\<subseteq>B\<^sub>2" using fun_inter_vimage_mono by simp_all
189+ thus "?B\<^sub>3\<subseteq>B\<^sub>1\<inter>B\<^sub>2" by auto
190+ qed
191+ ultimately show "\<exists>B\<in>\<BB>. B\<subseteq>B\<^sub>1\<inter>B\<^sub>2" by ( rule witness_exists )
192+ qed
193+
194+ end
0 commit comments