Theory UniformSpace_ZF
section ‹Uniform spaces›
theory UniformSpace_ZF imports Cardinal_ZF Order_ZF_1a Topology_ZF_2 Topology_ZF_4a
begin
text‹ This theory defines uniform spaces and proves their basic properties. ›
subsection‹ Entourages and neighborhoods ›
text‹ Just like a topological space constitutes the minimal setting
in which one can speak of continuous functions, the notion of uniform spaces
(commonly attributed to André Weil) captures the minimal setting in which one can speak
of uniformly continuous functions.
In some sense this is a generalization of the notion of metric (or metrizable)
spaces and topological groups. ›
text‹ There are several definitions of uniform spaces.
The fact that these definitions are equivalent is far from obvious
(some people call such phenomenon cryptomorphism).
We will use the definition of the uniform structure (or ''uniformity'')
based on entourages. This was the original definition by Weil and it seems
to be the most commonly used.
A uniformity consists of entourages that are binary relations between points of space $X$
that satisfy a certain collection of conditions, specified below. ›
definition
IsUniformity ("_ {is a uniformity on} _" 90) where
"Φ {is a uniformity on} X ≡(Φ {is a filter on} (X×X))
∧ (∀U∈Φ. id(X) ⊆ U ∧ (∃V∈Φ. V O V ⊆ U) ∧ converse(U) ∈ Φ)"
text‹Since the whole $X\times X$ is in a uniformity, a uniformity is never empty.›
lemma uniformity_non_empty: assumes "Φ {is a uniformity on} X"
shows "Φ≠∅"
using assms unfolding IsUniformity_def IsFilter_def by auto
text‹ If $\Phi$ is a uniformity on $X$, then the every element $V$ of $\Phi$
is a certain relation on $X$ (a subset of $X\times X$) and is called
an ''entourage''. For an $x\in X$ we call $V\{ x\}$ a neighborhood of $x$.
The first useful fact we will show is that neighborhoods are non-empty. ›
lemma neigh_not_empty:
assumes "Φ {is a uniformity on} X" "W∈Φ" and "x∈X"
shows "W``{x} ≠ ∅" and "x ∈ W``{x}"
proof -
from assms(1,2) have "id(X) ⊆ W"
unfolding IsUniformity_def IsFilter_def by auto
with ‹x∈X› show" x∈W``{x}" and "W``{x} ≠ ∅" by auto
qed
text‹The filter part of the definition of uniformity for easier reference:›
lemma unif_filter: assumes "Φ {is a uniformity on} X"
shows "Φ {is a filter on} (X×X)"
using assms unfolding IsUniformity_def by simp
text‹If $X$ is not empty then the singleton $\{ X\times X\}$ is a (trivial)
example of a uniformity on $X$. ›
lemma min_uniformity: assumes "X≠∅" shows "{X×X} {is a uniformity on} X"
using assms unfolding IsFilter_def IsUniformity_def by auto
text‹On the other side of the spectrum is the collection of sets containing the
diagonal, that is also a uniformity.›
lemma max_uniformity: assumes "X≠∅"
shows "{U∈Pow(X×X). id(X)⊆U} {is a uniformity on} X"
using assms unfolding IsFilter_def IsUniformity_def by auto
text‹The second part of the definition of uniformity for easy reference:›
lemma entourage_props:
assumes "Φ {is a uniformity on} X" and "A∈Φ"
shows
"A ⊆ X×X"
"id(X) ⊆ A"
"∃V∈Φ. V O V ⊆ A"
"converse(A) ∈ Φ"
proof -
from assms show "id(X) ⊆ A" "∃V∈Φ. V O V ⊆ A" "converse(A) ∈ Φ"
unfolding IsUniformity_def by auto
from assms show "A ⊆ X×X"
using unif_filter unfolding IsFilter_def by blast
qed
text‹The definition of uniformity states (among other things) that for every member $U$
of uniformity $\Phi$ there is another one, say $V$ such that $V\circ V\subseteq U$. Sometimes such $V$
is said to be half the size of $U$. The next lemma states that $V$ can be taken to be symmetric. ›
lemma half_size_symm: assumes "Φ {is a uniformity on} X" "W∈Φ"
shows "∃V∈Φ. V O V ⊆ W ∧ V=converse(V)"
proof -
from assms obtain U where "U∈Φ" and "U O U ⊆ W"
unfolding IsUniformity_def by auto
let ?V = "U ∩ converse(U)"
from assms(1) ‹U∈Φ› have "?V ∈ Φ" and "?V = converse(?V)"
unfolding IsUniformity_def IsFilter_def by auto
moreover from ‹U O U ⊆ W› have "?V O ?V ⊆ W" by auto
ultimately show ?thesis by blast
qed
text‹Inside every member $W$ of the uniformity $\Phi$ we can find one that is symmetric and
smaller than a third of size $W$. Compare with the Metamath's theorem with the same name.›
lemma ustex3sym: assumes "Φ {is a uniformity on} X" "A∈Φ"
shows "∃B∈Φ. B O (B O B) ⊆ A ∧ B=converse(B)"
proof -
from assms obtain C where "C∈Φ" and "C O C ⊆ A"
unfolding IsUniformity_def by auto
from assms(1) ‹C∈Φ› obtain B where
"B∈Φ" "B O B ⊆ C" and "B=converse(B)"
using half_size_symm by blast
with ‹C O C ⊆ A› have "(B O B) O (B O B) ⊆ A" by blast
with assms(1) ‹B∈Φ› have "B O (B O B) ⊆ A"
using entourage_props(1,2) by blast
with ‹B∈Φ› ‹B=converse(B)› show ?thesis by blast
qed
text‹If $\Phi$ is a uniformity on $X$ then every element of $\Phi$ is a subset of $X\times X$
whose domain is $X$. ›
lemma uni_domain:
assumes "Φ {is a uniformity on} X" "W∈Φ"
shows "W ⊆ X×X" and "domain(W) = X"
proof -
from assms show "W ⊆ X×X" unfolding IsUniformity_def IsFilter_def
by blast
show "domain(W) = X"
proof
from assms show "domain(W) ⊆ X" unfolding IsUniformity_def IsFilter_def
by auto
from assms show "X ⊆ domain(W)" unfolding IsUniformity_def by blast
qed
qed
text‹If $\Phi$ is a uniformity on $X$ and $W\in \Phi$ the for every $x\in X$
the image of the singleton $\{ x\}$ by $W$ is contained in $X$. Compare
the Metamath's theorem with the same name. ›
lemma ustimasn:
assumes "Φ {is a uniformity on} X" "W∈Φ" and "x∈X"
shows "W``{x} ⊆ X"
using assms uni_domain(1) by auto
text‹ Uniformity ‹Φ› defines a natural topology on its space $X$ via the neighborhood system
that assigns the collection $\{V(\{x\}):V\in \Phi\}$ to every point $x\in X$.
In the next lemma we show that if we define a function
this way the values of that function are what they should be. This is only a technical
fact which is useful to shorten the remaining proofs, usually treated as obvious in standard
mathematics. ›
lemma neigh_filt_fun:
assumes "Φ {is a uniformity on} X"
defines "ℳ ≡ {⟨x,{V``{x}.V∈Φ}⟩.x∈X}"
shows "ℳ:X→Pow(Pow(X))" and "∀x∈X. ℳ`(x) = {V``{x}.V∈Φ}"
proof -
from assms have "∀x∈X. {V``{x}.V∈Φ} ∈ Pow(Pow(X))"
using IsUniformity_def IsFilter_def image_subset by auto
with assms show "ℳ:X→Pow(Pow(X))" using ZF_fun_from_total by simp
with assms show "∀x∈X. ℳ`(x) = {V``{x}.V∈Φ}" using ZF_fun_from_tot_val
by simp
qed
text‹ In the next lemma we show that the collection defined in lemma ‹neigh_filt_fun› is a filter on $X$.
The proof is kind of long, but it just checks that all filter conditions hold.›
lemma filter_from_uniformity:
assumes "Φ {is a uniformity on} X" and "x∈X"
defines "ℳ ≡ {⟨x,{V``{x}.V∈Φ}⟩.x∈X}"
shows "ℳ`(x) {is a filter on} X"
proof -
from assms have PhiFilter: "Φ {is a filter on} (X×X)" and
"ℳ:X→Pow(Pow(X))" and "ℳ`(x) = {V``{x}.V∈Φ}"
using IsUniformity_def neigh_filt_fun by auto
have "∅ ∉ ℳ`(x)"
proof -
from assms ‹x∈X› have "∅ ∉ {V``{x}.V∈Φ}" using neigh_not_empty by blast
with ‹ℳ`(x) = {V``{x}.V∈Φ}› show "∅ ∉ ℳ`(x)" by simp
qed
moreover have "X ∈ ℳ`(x)"
proof -
note ‹ℳ`(x) = {V``{x}.V∈Φ}›
moreover from assms have "X×X ∈ Φ" unfolding IsUniformity_def IsFilter_def
by blast
hence "(X×X)``{x} ∈ {V``{x}.V∈Φ}" by auto
moreover from ‹x∈X› have "(X×X)``{x} = X" by auto
ultimately show "X ∈ ℳ`(x)" by simp
qed
moreover from ‹ℳ:X→Pow(Pow(X))› ‹x∈X› have "ℳ`(x) ⊆ Pow(X)" using apply_funtype
by blast
moreover have LargerIn: "∀B ∈ ℳ`(x). ∀C ∈ Pow(X). B⊆C ⟶ C ∈ ℳ`(x)"
proof -
{ fix B assume "B ∈ ℳ`(x)"
fix C assume "C ∈ Pow(X)" and "B⊆C"
from ‹ℳ`(x) = {V``{x}.V∈Φ}› ‹B ∈ ℳ`(x)› obtain U where
"U∈Φ" and "B = U``{x}" by auto
let ?V = "U ∪ C×C"
from assms ‹U∈Φ› ‹C ∈ Pow(X)› have "?V ∈ Pow(X×X)" and "U⊆?V"
using IsUniformity_def IsFilter_def by auto
with ‹U∈Φ› PhiFilter have "?V∈Φ" using IsFilter_def by simp
moreover from assms ‹U∈Φ› ‹x∈X› ‹B = U``{x}› ‹B⊆C› have "C = ?V``{x}"
using neigh_not_empty image_greater_rel by simp
ultimately have "C ∈ {V``{x}.V∈Φ}" by auto
with ‹ℳ`(x) = {V``{x}.V∈Φ}› have "C ∈ ℳ`(x)" by simp
} thus ?thesis by blast
qed
moreover have "∀A ∈ ℳ`(x).∀B ∈ ℳ`(x). A∩B ∈ ℳ`(x)"
proof -
{ fix A B assume "A ∈ ℳ`(x)" and "B ∈ ℳ`(x)"
with ‹ℳ`(x) = {V``{x}.V∈Φ}› obtain V⇩A V⇩B where
"A = V⇩A``{x}" "B = V⇩B``{x}" and "V⇩A ∈ Φ" "V⇩B ∈ Φ"
by auto
let ?C = "V⇩A``{x} ∩ V⇩B``{x}"
from assms ‹V⇩A ∈ Φ› ‹V⇩B ∈ Φ› have "V⇩A∩V⇩B ∈ Φ" using IsUniformity_def IsFilter_def
by simp
with ‹ℳ`(x) = {V``{x}.V∈Φ}› have "(V⇩A∩V⇩B)``{x} ∈ ℳ`(x)" by auto
moreover from PhiFilter ‹V⇩A ∈ Φ› ‹V⇩B ∈ Φ› have "?C ∈ Pow(X)" unfolding IsFilter_def
by auto
moreover have "(V⇩A∩V⇩B)``{x} ⊆ ?C" using image_Int_subset_left by simp
moreover note LargerIn
ultimately have "?C ∈ ℳ`(x)" by simp
with ‹A = V⇩A``{x}› ‹B = V⇩B``{x}› have "A∩B ∈ ℳ`(x)" by blast
} thus ?thesis by simp
qed
ultimately show ?thesis unfolding IsFilter_def by simp
qed
text‹A rephrasing of ‹filter_from_uniformity›: if $\Phi$ is a uniformity on $X$,
then $\{V(\{ x\}) | V\in \Phi\}$ is a filter on $X$ for every $x\in X$.›
lemma unif_filter_at_point:
assumes "Φ {is a uniformity on} X" and "x∈X"
shows "{V``{x}.V∈Φ} {is a filter on} X"
using assms filter_from_uniformity ZF_fun_from_tot_val1
by simp
text‹A frequently used property of filters is that they are "upward closed" i.e. supersets
of a filter element are also in the filter. The next lemma makes this explicit
for easy reference as applied to the natural filter created from a uniformity.›
corollary unif_filter_up_closed:
assumes "Φ {is a uniformity on} X" "x∈X" "U ∈ {V``{x}. V∈Φ}" "W⊆X" "U⊆W"
shows "W ∈ {V``{x}.V∈Φ}"
using assms filter_from_uniformity ZF_fun_from_tot_val1
unfolding IsFilter_def by auto
text‹ The function defined in the premises of lemma ‹neigh_filt_fun›
(or ‹filter_from_uniformity›) is a neighborhood system. The proof uses the existence
of the "half-the-size" neighborhood condition (‹∃V∈Φ. V O V ⊆ U›) of the uniformity definition,
but not the ‹converse(U) ∈ Φ› part. ›
theorem neigh_from_uniformity:
assumes "Φ {is a uniformity on} X"
shows "{⟨x,{V``{x}.V∈Φ}⟩.x∈X} {is a neighborhood system on} X"
proof -
let ?ℳ = "{⟨x,{V``{x}.V∈Φ}⟩.x∈X}"
from assms have "?ℳ:X→Pow(Pow(X))" and Mval: "∀x∈X. ?ℳ`(x) = {V``{x}.V∈Φ}"
using IsUniformity_def neigh_filt_fun by auto
moreover from assms have "∀x∈X. (?ℳ`(x) {is a filter on} X)" using filter_from_uniformity
by simp
moreover
{ fix x assume "x∈X"
have "∀N∈?ℳ`(x). x∈N ∧ (∃U∈?ℳ`(x).∀y∈U.(N∈?ℳ`(y)))"
proof -
{ fix N assume "N∈?ℳ`(x)"
have "x∈N" and "∃U∈?ℳ`(x).∀y∈U.(N ∈ ?ℳ`(y))"
proof -
from ‹?ℳ:X→Pow(Pow(X))› Mval ‹x∈X› ‹N∈?ℳ`(x)›
obtain U where "U∈Φ" and "N = U``{x}" by auto
with assms ‹x∈X› show "x∈N" using neigh_not_empty by simp
from assms ‹U∈Φ› obtain V where "V∈Φ" and "V O V ⊆ U"
unfolding IsUniformity_def by auto
let ?W = "V``{x}"
from ‹V∈Φ› Mval ‹x∈X› have "?W ∈ ?ℳ`(x)" by auto
moreover have "∀y∈?W. N ∈ ?ℳ`(y)"
proof -
{ fix y assume "y∈?W"
with ‹?ℳ:X→Pow(Pow(X))› ‹x∈X› ‹?W ∈ ?ℳ`(x)› have "y∈X"
using apply_funtype by blast
with assms have "?ℳ`(y) {is a filter on} X" using filter_from_uniformity
by simp
moreover from assms ‹y∈X› ‹V∈Φ› have "V``{y} ∈ ?ℳ`(y)"
using neigh_filt_fun by auto
moreover from ‹?ℳ:X→Pow(Pow(X))› ‹x∈X› ‹N ∈ ?ℳ`(x)›
have "N ∈ Pow(X)" using apply_funtype by blast
moreover from ‹V O V ⊆ U› ‹y∈?W› have
"V``{y} ⊆ (V O V)``{x}" and "(V O V)``{x} ⊆ U``{x}"
by auto
with ‹N = U``{x}› have "V``{y} ⊆ N" by blast
ultimately have "N ∈ ?ℳ`(y)" unfolding IsFilter_def by simp
} thus ?thesis by simp
qed
ultimately show "∃U∈?ℳ`(x).∀y∈U.(N ∈ ?ℳ`(y))" by auto
qed
} thus ?thesis by simp
qed
}
ultimately show ?thesis unfolding IsNeighSystem_def by simp
qed
text‹ When we have a uniformity $\Phi$ on $X$ we can define a topology on $X$ in a (relatively)
natural way. We will call that topology the ‹ UniformTopology(Φ)›.
We could probably reformulate the definition to skip
the $X$ parameter because if $\Phi$ is a uniformity on $X$ then $X$ can be recovered
from (is determined by) $\Phi$. ›
definition
"UniformTopology(Φ,X) ≡ {U∈Pow(X). ∀x∈U. U∈{V``{x}. V∈Φ}}"
text‹An identity showing how the definition of uniform topology is constructed.
Here, the $M = \{\langle t,\{ V\{ t\} : V\in \Phi\}\rangle : t\in X\}$ is the neighborhood system
(a function on $X$) created from uniformity $\Phi$.
Then for each $x\in X$, $M(x) = \{ V\{ t\} : V\in \Phi\}$ is the set of neighborhoods of $x$. ›
lemma uniftop_def_alt:
shows "UniformTopology(Φ,X) = {U ∈ Pow(X). ∀x∈U. U ∈ {⟨t,{V``{t}.V∈Φ}⟩.t∈X}`(x)}"
proof -
let ?ℳ = "{⟨x,{V``{x}. V∈Φ}⟩. x∈X}"
have "∀U∈Pow(X).∀x∈U. ?ℳ`(x) = {V``{x}. V∈Φ}"
using ZF_fun_from_tot_val1 by auto
then show ?thesis unfolding UniformTopology_def by auto
qed
text‹ The collection of sets constructed in the ‹ UniformTopology › definition
is indeed a topology on $X$. ›
theorem uniform_top_is_top:
assumes "Φ {is a uniformity on} X"
shows
"UniformTopology(Φ,X) {is a topology}" and "⋃ UniformTopology(Φ,X) = X"
using assms neigh_from_uniformity uniftop_def_alt topology_from_neighs
by auto
text‹If we have a uniformity $\Phi$ we can create a neighborhood system from it in two ways.
We can create a a neighborhood system directly from $\Phi$ using the formula
$X \ni x \mapsto \{V\{x\} | V\in \Phi\}$ (see theorem ‹neigh_from_uniformity›).
Alternatively we can construct a topology from $\Phi$ as in theorem
‹uniform_top_is_top› and then create a neighborhood system from this topology
as in theorem ‹neigh_from_topology›. The next theorem states that these two ways give the same
result. ›
theorem neigh_unif_same: assumes "Φ {is a uniformity on} X"
shows
"{⟨x,{V``{x}.V∈Φ}⟩. x∈X} = {neighborhood system of} UniformTopology(Φ,X)"
using assms neigh_from_uniformity nei_top_nei_round_trip uniftop_def_alt
by simp
text‹Another form of the definition of topology generated from a uniformity.›
lemma uniftop_def_alt1: assumes "Φ {is a uniformity on} X"
shows "UniformTopology(Φ,X) = {U∈Pow(X). ∀x∈U. ∃W∈Φ. W``{x} ⊆ U}"
proof
let ?T = "UniformTopology(Φ,X)"
show "?T ⊆ {U∈Pow(X). ∀x∈U. ∃W∈Φ. W``{x} ⊆ U}"
unfolding UniformTopology_def by auto
{ fix U assume "U∈{U∈Pow(X). ∀x∈U. ∃W∈Φ. W``{x} ⊆ U}"
then have "U∈Pow(X)" and I: "∀x∈U. ∃W∈Φ. W``{x} ⊆ U" by auto
{ fix x assume "x∈U"
with I obtain W where "W∈Φ" and "W``{x} ⊆ U"
by auto
let ?𝔉 = "{V``{x}.V∈Φ}"
from assms(1) ‹U∈Pow(X)› ‹x∈U› ‹W∈Φ› have
"?𝔉 {is a filter on} X" and "W``{x} ∈ ?𝔉"
using unif_filter_at_point by auto
with ‹U∈Pow(X)› ‹W``{x} ⊆ U› have "U∈?𝔉"
using is_filter_def_split(5) by blast
} hence "∀x∈U. U ∈ {V``{x}.V∈Φ}" by simp
with ‹U∈Pow(X)› have "U∈?T"
unfolding UniformTopology_def by simp
} thus "{U∈Pow(X). ∀x∈U. ∃W∈Φ. W``{x} ⊆ U} ⊆ ?T"
by blast
qed
text‹Images of singletons by entourages are neighborhoods of those singletons.›
lemma image_singleton_ent_nei:
assumes "Φ {is a uniformity on} X" "V∈Φ" "x∈X"
defines "ℳ ≡ {neighborhood system of} UniformTopology(Φ,X)"
shows "V``{x} ∈ ℳ`(x)"
proof -
from assms(1,4) have "ℳ = {⟨x,{V``{x}.V∈Φ}⟩. x∈X}"
using neigh_unif_same by simp
with assms(2,3) show ?thesis
using ZF_fun_from_tot_val1 by auto
qed
text‹The set neighborhoods of a singleton $\{ x\}$ where $x\in X$ consist
of images of the singleton by the entourages $W\in \Phi$.
See also the Metamath's theorem with the same name. ›
lemma utopsnneip: assumes "Φ {is a uniformity on} X" "x∈X"
defines "𝒮 ≡ {set neighborhood system of} UniformTopology(Φ,X)"
shows "𝒮`{x} = {W``{x}. W∈Φ}"
proof -
let ?T = "UniformTopology(Φ,X)"
let ?ℳ = "{neighborhood system of} ?T"
from assms(1,2) have "x ∈ ⋃?T"
using uniform_top_is_top(2) by simp
with assms(3) have "?ℳ`(x) = 𝒮`{x}"
using neigh_from_nei by simp
moreover
from assms(1) have "?ℳ = {⟨x,{W``{x}.W∈Φ}⟩. x∈X}"
using neigh_unif_same by simp
with assms(2) have "?ℳ`(x) = {W``{x}.W∈Φ}"
using ZF_fun_from_tot_val1 by simp
ultimately show ?thesis by simp
qed
text‹Images of singletons by entourages are set neighborhoods of those singletons.
See also the Metamath theorem with the same name.›
corollary utopsnnei: assumes "Φ {is a uniformity on} X" "W∈Φ" "x∈X"
defines "𝒮 ≡ {set neighborhood system of} UniformTopology(Φ,X)"
shows "W``{x} ∈ 𝒮`{x}" using assms utopsnneip by auto
text‹If $\Phi$ is a uniformity on $X$ that generates a topology $T$, $R$ is any relation
on $X$ (i.e. $R\subseteq X\times X$), $W$ is a symmetric entourage (i.e. $W\in \Phi$,
and $W$ is symmetric (i.e. equal to its converse)), then the closure of $R$ in the product topology
is contained the the composition $V\circ (M \circ V)$.
Metamath has a similar theorem with the same name. ›
lemma utop3cls:
assumes "Φ {is a uniformity on} X" "R⊆X×X" "W∈Φ" "W=converse(W)"
defines "J ≡ UniformTopology(Φ,X)"
shows "Closure(R,J×⇩tJ) ⊆ W O (R O W)"
proof
let ?M = "{set neighborhood system of} (J×⇩tJ)"
fix z assume zMem: "z ∈ Closure(R,J×⇩tJ)"
from assms(1,5) have Jtop: "J {is a topology}" and "⋃J = X"
using uniform_top_is_top by auto
then have JJtop: "(J×⇩tJ) {is a topology}" and JxJ: "⋃(J×⇩tJ) = X×X"
using Top_1_4_T1(1,3) by auto
with assms(2) have "topology0(J×⇩tJ)" and "R ⊆ ⋃(J×⇩tJ)"
unfolding topology0_def by auto
then have "Closure(R,J×⇩tJ) ⊆ ⋃(J×⇩tJ)"
using topology0.Top_3_L11(1) by simp
with ‹z ∈ Closure(R,J×⇩tJ)› JxJ have "z∈X×X" by auto
let ?x = "fst(z)"
let ?y = "snd(z)"
from ‹z∈X×X› have "?x∈X" "?y∈X" "z = ⟨?x,?y⟩" by auto
with assms(1,3,5) Jtop have "(W``{?x})×(W``{?y}) ∈ ?M`({?x}×{?y})"
using utopsnnei neitx by simp
moreover from ‹z = ⟨?x,?y⟩› have "{?x}×{?y} = {z}"
by (rule pair_prod)
ultimately have "(W``{?x})×(W``{?y}) ∈ ?M`{z}" by simp
with zMem JJtop ‹R ⊆ ⋃(J×⇩tJ)› have "(W``{?x})×(W``{?y}) ∩ R ≠ ∅"
using neindisj by blast
with assms(4) have "⟨?x,?y⟩ ∈ W O (R O W)"
using sym_rel_comp by simp
with ‹z = ⟨?x,?y⟩› show "z ∈ W O (R O W)"
by simp
qed
text‹Uniform spaces are regular. Note that is not the same as $T_3$, see ‹Topology_ZF_1›
for separation axioms definitions. In some sources the definitions of "regular" and $T_3$
are swapped. In IsarMathLib we adopt the terminology as on the "Separation axiom"
page on Wikipedia.›
theorem utopreg:
assumes "Φ {is a uniformity on} X"
shows "UniformTopology(Φ,X) {is regular}"
proof -
let ?J = "UniformTopology(Φ,X)"
let ?𝒮 = "{set neighborhood system of} ?J"
from assms have "⋃?J = X"
and Jtop: "?J {is a topology}" and cntx: "topology0(?J)"
using uniform_top_is_top unfolding topology0_def by auto
have "∀U∈?J. ∀x∈U. ∃V∈?J. x∈V ∧ Closure(V,?J)⊆U"
proof -
{ fix U x assume "U∈?J" "x∈U"
then have "U ∈ ?𝒮`{x}" using open_nei_singl by simp
from ‹U∈?J› have "U⊆⋃?J" by auto
with ‹x∈U› ‹⋃?J = X› have "x∈X" by auto
from assms(1) ‹x∈X› ‹U ∈ ?𝒮`{x}› obtain A
where "U=A``{x}" and "A∈Φ"
using utopsnneip by auto
from assms(1) ‹A∈Φ› obtain W where
"W∈Φ" "W O (W O W) ⊆ A" and Wsymm: "W=converse(W)"
using ustex3sym by blast
with assms(1) ‹x∈X› have "W``{x} ∈ ?𝒮`{x}" and "W``{x} ⊆ X"
using utopsnnei ustimasn by auto
from ‹W``{x} ∈ ?𝒮`{x}› have "∃V∈?J. {x}⊆V ∧ V⊆W``{x}"
by (rule neii2)
then obtain V where "V∈?J" "x∈V" "V⊆W``{x}"
by blast
have "Closure(V,?J) ⊆ U"
proof -
from assms(1) ‹W∈Φ› ‹⋃?J = X› have "W ⊆ X×X"
using entourage_props(1) by simp
from cntx ‹W``{x} ⊆ X› ‹⋃?J = X› ‹V⊆W``{x}›
have "Closure(V,?J) ⊆ Closure(W``{x},?J)"
using topology0.top_closure_mono by simp
also have "Closure(W``{x},?J) ⊆ Closure(W,?J×⇩t?J)``{x}"
proof -
from ‹W⊆X×X› ‹x∈X› ‹⋃?J = X›
have "W⊆(⋃?J)×(⋃?J)" "x∈⋃?J" by auto
with ‹?J {is a topology}› show ?thesis
using imasncls by simp
qed
also from assms(1) ‹W⊆X×X› ‹W∈Φ› Wsymm ‹W O (W O W) ⊆ A›
have "Closure(W,?J×⇩t?J)``{x} ⊆ A``{x}"
using utop3cls by blast
finally have "Closure(V,?J) ⊆ A``{x}"
by simp
with ‹U=A``{x}› show ?thesis by auto
qed
with ‹V∈?J› ‹x∈V› have "∃V∈?J. x∈V ∧ Closure(V,?J)⊆U"
by blast
} thus ?thesis by simp
qed
with Jtop show "?J {is regular}" using is_regular_def_alt
by simp
qed
text‹If the topological space generated by a uniformity $\Phi$ on $X$ is $T_1$
then the intersection $\bigcup \Phi$ is contained in the diagonal
$\{\langle x,x\rangle : x\in X\}$. Note the opposite inclusion is true for every uniformity.›
lemma unif_t1_inter_diag:
assumes "Φ {is a uniformity on} X" and "UniformTopology(Φ,X) {is T⇩1}"
shows "⋂Φ ⊆ {⟨x,x⟩. x∈X}"
proof -
let ?T = "UniformTopology(Φ,X)"
from assms(1) have "⋂Φ ⊆ X×X" using uniformity_non_empty entourage_props(1)
by blast
{ fix p assume "p ∈ ⋂Φ" and "p ∉ {⟨x,x⟩. x∈X}"
from ‹⋂Φ ⊆ X×X› ‹p ∈ ⋂Φ› obtain x y where "x∈X" "y∈X" "p = ⟨x,y⟩" by auto
with assms ‹p ∉ {⟨x,x⟩. x∈X}› obtain U where "U ∈ ?T" "x∈U" "y∉U"
using uniform_top_is_top(2) unfolding isT1_def by force
with assms(1) ‹p = ⟨x,y⟩› ‹p ∈ ⋂Φ› have False
using uniftop_def_alt1 by force
} with ‹⋂Φ ⊆ X×X› show ?thesis by blast
qed
text‹If the intersection of a uniformity is contained in the the diagonal
$\{\langle x,x\rangle : x\in X\}$ then the topological space generated by this uniformity
is $T_1$.›
lemma unif_inter_diag_t1:
assumes "Φ {is a uniformity on} X" and "⋂Φ ⊆ {⟨x,x⟩. x∈X}"
shows "UniformTopology(Φ,X) {is T⇩1}"
proof -
let ?T = "UniformTopology(Φ,X)"
let ?ℳ = "{neighborhood system of} ?T"
from assms(1) have "⋃?T = X" using uniform_top_is_top(2) by simp
{ fix x y assume "x∈X" "y∈X" "x≠y"
with assms obtain W where "W∈Φ" and "y∉W``{x}"
using uniformity_non_empty by blast
from assms(1) ‹x∈X› ‹W∈Φ› have "W``{x} ∈ ?ℳ`(x)"
using image_singleton_ent_nei by simp
with ‹x∈X› ‹⋃?T = X› ‹y∉W``{x}› have "∃U∈?T. x∈U ∧ y∉U"
using neigh_val by auto
} with ‹⋃?T = X› show ?thesis unfolding isT1_def by simp
qed
text‹If $\Phi$ is a uniformity on $X$ then the intersection of $\Phi$ is contained in
diagonal of $X$ if and only if $\bigcup \Phi$ is equal to that diagonal. Some people call
such uniform space "separating".›
theorem unif_inter_diag: assumes "Φ {is a uniformity on} X"
shows "⋂Φ ⊆ {⟨x,x⟩. x∈X} ⟷ ⋂Φ = {⟨x,x⟩. x∈X}"
using assms entourage_props(2) uniformity_non_empty by force
text‹The next theorem collects the information we have to show that
if $\Phi$ is a uniformity on $X$, with the induced topology $T$ then
conditions $T$ is $T_0$, $T$ is $T_1$, $T$ is $T_2$ $T$ is $T_3$ are all equivalent to
the intersection of $\Phi$ being contained in the diagonal
(which is equivalent to the intersection of $\Phi$ being equal to the diagonal, see
‹unif_inter_diag› above.›
theorem unif_sep_axioms_diag: assumes "Φ {is a uniformity on} X"
defines "T ≡ UniformTopology(Φ,X)"
shows
"⋂Φ ⊆ {⟨x,x⟩. x∈X} ⟷ T {is T⇩0}"
"⋂Φ ⊆ {⟨x,x⟩. x∈X} ⟷ T {is T⇩1}"
"⋂Φ ⊆ {⟨x,x⟩. x∈X} ⟷ T {is T⇩2}"
"⋂Φ ⊆ {⟨x,x⟩. x∈X} ⟷ T {is T⇩3}"
proof -
from assms show "⋂Φ ⊆ {⟨x,x⟩. x∈X} ⟷ T {is T⇩1}"
using unif_t1_inter_diag unif_inter_diag_t1 by auto
with assms show
"⋂Φ ⊆ {⟨x,x⟩. x∈X} ⟷ T {is T⇩0}"
"⋂Φ ⊆ {⟨x,x⟩. x∈X} ⟷ T {is T⇩2}"
"⋂Φ ⊆ {⟨x,x⟩. x∈X} ⟷ T {is T⇩3}"
using utopreg T1_is_T0 T3_is_T2 T2_is_T1
unfolding isT3_def by auto
qed
subsection‹ Base of a uniformity ›
text‹A ‹base› or a ‹fundamental system of entourages› of a uniformity $\Phi$ is
a subset of $\Phi$ that is sufficient to uniquely determine it. This is
analogous to the notion of a base of a topology (see ‹Topology_ZF_1› or a base of a filter
(see ‹Topology_ZF_4›). ›
text‹A base of a uniformity $\Phi$ is any subset $\mathfrak{B}\subseteq \Phi$ such that
every entourage in $\Phi$ contains (at least) one from $\mathfrak{B}$.
The phrase ‹is a base for› is already defined to mean a base for a topology,
so we use the phrase ‹is a uniform base of› here. ›
definition
IsUniformityBase ("_ {is a uniform base of} _" 90) where
"𝔅 {is a uniform base of} Φ ≡ 𝔅 ⊆ Φ ∧ (∀U∈Φ. ∃B∈𝔅. B⊆U)"
text‹Symmetric entourages form a base of the uniformity.›
lemma symm_are_base: assumes "Φ {is a uniformity on} X"
shows "{V∈Φ. V = converse(V)} {is a uniform base of} Φ"
proof -
let ?𝔅 = "{V∈Φ. V = converse(V)}"
{ fix W assume "W∈Φ"
with assms obtain V where "V∈Φ" "V O V ⊆ W" "V=converse(V)"
using half_size_symm by blast
from assms ‹V∈Φ› have "V ⊆ V O V"
using entourage_props(1,2) refl_square_greater by blast
with ‹V O V ⊆ W› ‹V∈Φ› ‹V=converse(V)› have "∃V∈?𝔅. V⊆W" by auto
} hence "∀W∈Φ. ∃V∈?𝔅. V ⊆ W" by auto
then show ?thesis unfolding IsUniformityBase_def by auto
qed
text‹Given a base of a uniformity we can recover the uniformity taking the supersets.
The ‹Supersets› constructor is defined in ‹ZF1›.›
lemma uniformity_from_base:
assumes "Φ {is a uniformity on} X" "𝔅 {is a uniform base of} Φ"
shows "Φ = Supersets(X×X,𝔅)"
proof
from assms show "Φ ⊆ Supersets(X×X,𝔅)"
unfolding IsUniformityBase_def Supersets_def
using entourage_props(1) by auto
from assms show "Supersets(X×X,𝔅) ⊆ Φ"
unfolding Supersets_def IsUniformityBase_def IsUniformity_def IsFilter_def
by auto
qed
text‹Analogous to the predicate "satisfies base condition" (defined in ‹Topology_ZF_1›)
and "is a base filter" (defined in ‹Topology_ZF_4›) we can specify conditions
for a collection $\mathfrak{B}$ of subsets of $X\times X$ to be a base of some
uniformity on $X$. Namely, the following conditions are necessary and sufficient:
1. Intersection of two sets of $\mathfrak{B}$ contains a set of $\mathfrak{B}$.
2. Every set of $\mathfrak{B}$ contains the diagonal of $X\times X$.
3. For each set $B_1\in \mathfrak{B}$ we can find a set $B_2\in \mathfrak{B}$
such that $B_2\subseteq B_1^{-1}$.
4. For each set $B_1\in \mathfrak{B}$ we can find a set $B_2\in \mathfrak{B}$
such that $B_2\circ B_2 \subseteq B_1$.
The conditions in the definition below are taken from
N. Bourbaki "Elements of Mathematics, General Topology", Chapter II.1.,
except for the last two that are missing there.›
definition
IsUniformityBaseOn ("_ {is a uniform base on} _" 90) where
"𝔅 {is a uniform base on} X ≡
(∀B⇩1∈𝔅. ∀B⇩2∈𝔅. ∃B⇩3∈𝔅. B⇩3⊆B⇩1∩B⇩2) ∧ (∀B∈𝔅. id(X)⊆B) ∧
(∀B⇩1∈𝔅. ∃B⇩2∈𝔅. B⇩2 ⊆ converse(B⇩1)) ∧ (∀B⇩1∈𝔅. ∃B⇩2∈𝔅. B⇩2 O B⇩2 ⊆ B⇩1) ∧
𝔅⊆Pow(X×X) ∧ 𝔅≠∅"
text‹The next lemma splits the definition of ‹IsUniformityBaseOn› into four conditions
to enable more precise references in proofs.›
lemma uniformity_base_props: assumes "𝔅 {is a uniform base on} X"
shows
"∀B⇩1∈𝔅. ∀B⇩2∈𝔅. ∃B⇩3∈𝔅. B⇩3⊆B⇩1∩B⇩2"
"∀B∈𝔅. id(X)⊆B"
"∀B⇩1∈𝔅. ∃B⇩2∈𝔅. B⇩2 ⊆ converse(B⇩1)"
"∀B⇩1∈𝔅. ∃B⇩2∈𝔅. B⇩2 O B⇩2 ⊆ B⇩1"
"𝔅⊆Pow(X×X)" and "𝔅≠∅"
using assms unfolding IsUniformityBaseOn_def by simp_all
text‹If supersets of some collection of subsets of $X\times X$ form a uniformity,
then this collection satisfies the conditions in the definition of ‹IsUniformityBaseOn›. ›
theorem base_is_uniform_base:
assumes "𝔅⊆Pow(X×X)" and "Supersets(X×X,𝔅) {is a uniformity on} X"
shows "𝔅 {is a uniform base on} X"
proof -
let ?Φ = "Supersets(X×X,𝔅)"
have "∀B⇩1∈𝔅. ∀B⇩2∈𝔅. ∃B⇩3∈𝔅. B⇩3⊆B⇩1∩B⇩2"
proof -
{ fix B⇩1 B⇩2 assume "B⇩1∈𝔅" "B⇩2∈𝔅"
with assms(1) have "B⇩1∈?Φ" and "B⇩2∈?Φ" unfolding Supersets_def by auto
with assms(2) have "∃B⇩3∈𝔅. B⇩3 ⊆ B⇩1∩B⇩2"
unfolding IsUniformity_def IsFilter_def Supersets_def by simp
} thus ?thesis by simp
qed
moreover have "∀B∈𝔅. id(X)⊆B"
proof -
{ fix B assume "B∈𝔅"
with assms(1) have "B∈?Φ" unfolding Supersets_def by auto
with assms(2) have "id(X)⊆B" unfolding IsUniformity_def by simp
} thus ?thesis by simp
qed
moreover have "∀B⇩1∈𝔅. ∃B⇩2∈𝔅. B⇩2 ⊆ converse(B⇩1)"
proof -
{ fix B⇩1 assume "B⇩1∈𝔅"
with assms(1) have "B⇩1∈?Φ" unfolding Supersets_def by auto
with assms have "∃B⇩2∈𝔅. B⇩2 ⊆ converse(B⇩1)"
unfolding IsUniformity_def Supersets_def by auto
} thus ?thesis by simp
qed
moreover have "∀B⇩1∈𝔅. ∃B⇩2∈𝔅. B⇩2 O B⇩2 ⊆ B⇩1"
proof -
{ fix B⇩1 assume "B⇩1∈𝔅"
with assms(1) have "B⇩1∈?Φ" unfolding Supersets_def by auto
with assms(2) obtain V where "V∈?Φ" and "V O V ⊆ B⇩1"
unfolding IsUniformity_def by blast
from assms(2) ‹V∈?Φ› obtain B⇩2 where "B⇩2∈𝔅" and "B⇩2⊆V"
unfolding Supersets_def by auto
from ‹V O V ⊆ B⇩1› ‹B⇩2⊆V› have "B⇩2 O B⇩2 ⊆ B⇩1" by auto
with ‹B⇩2∈𝔅› have "∃B⇩2∈𝔅. B⇩2 O B⇩2 ⊆ B⇩1" by auto
} thus ?thesis by simp
qed
moreover from assms(2) have "𝔅≠∅"
using supersets_of_empty uniformity_non_empty by blast
ultimately show "𝔅 {is a uniform base on} X"
unfolding IsUniformityBaseOn_def using assms(1) by simp
qed
text‹if a nonempty collection of subsets of $X\times X$ satisfies conditions in the definition
of ‹IsUniformityBaseOn› then the supersets of that collection form a uniformity on $X$.›
theorem uniformity_base_is_base:
assumes "X≠∅" and "𝔅 {is a uniform base on} X"
shows "Supersets(X×X,𝔅) {is a uniformity on} X"
proof -
let ?Φ = "Supersets(X×X,𝔅)"
from assms(2) have "𝔅⊆Pow(X×X)" using uniformity_base_props(5)
by simp
have "?Φ {is a filter on} (X×X)"
proof -
from assms have "∅∉?Φ"
unfolding Supersets_def using uniformity_base_props(2)
by blast
moreover have "X×X ∈ ?Φ"
proof -
from assms(2) obtain B where "B∈𝔅"
using uniformity_base_props(6) by blast
with ‹𝔅⊆Pow(X×X)› show "X×X ∈ ?Φ" unfolding Supersets_def
by blast
qed
moreover have "?Φ ⊆ Pow(X×X)" unfolding Supersets_def by auto
moreover have "∀U∈?Φ. ∀V∈?Φ. U∩V ∈ ?Φ"
proof -
{ fix U V assume "U∈?Φ" "V∈?Φ"
then obtain B⇩1 B⇩2 where "B⇩1∈𝔅" "B⇩2∈𝔅" "B⇩1⊆U" "B⇩2⊆V"
unfolding Supersets_def by auto
from assms(2) ‹B⇩1∈𝔅› ‹B⇩2∈𝔅› obtain B⇩3 where "B⇩3∈𝔅" and "B⇩3⊆B⇩1∩B⇩2"
using uniformity_base_props(1) by blast
from ‹B⇩1⊆U› ‹B⇩2⊆V› ‹B⇩3⊆B⇩1∩B⇩2› have "B⇩3⊆U∩V" by auto
with ‹U∈?Φ› ‹V∈?Φ› ‹B⇩3∈𝔅› have "U∩V ∈ ?Φ"
unfolding Supersets_def by auto
} thus ?thesis by simp
qed
moreover have "∀U∈?Φ. ∀C∈Pow(X×X). U⊆C ⟶ C∈?Φ"
proof -
{ fix U C assume "U∈?Φ" "C∈Pow(X×X)" "U⊆C"
from ‹U∈?Φ› obtain B where "B∈𝔅" and "B⊆U"
unfolding Supersets_def by auto
with ‹U⊆C› ‹C∈Pow(X×X)› have "C∈?Φ"
unfolding Supersets_def by auto
} thus ?thesis by auto
qed
ultimately show "?Φ {is a filter on} (X×X)"
unfolding IsFilter_def by simp
qed
moreover have "∀U∈?Φ. id(X)⊆U ∧ (∃V∈?Φ. V O V ⊆ U) ∧ converse(U)∈?Φ"
proof -
{ fix U assume "U∈?Φ"
then obtain B where "B∈𝔅" and "B⊆U"
unfolding Supersets_def by auto
with assms(2) have "id(X) ⊆ U"
using uniformity_base_props(2) by blast
moreover
from assms(2) ‹B∈𝔅› obtain V where "V∈𝔅" and "V O V ⊆ B"
using uniformity_base_props(4) by blast
with ‹𝔅⊆Pow(X×X)› have "V∈?Φ" using superset_gen by auto
with ‹V O V ⊆ B› ‹B⊆U› have "∃V∈?Φ. V O V ⊆ U" by blast
moreover
from assms(2) ‹B∈𝔅› ‹B⊆U› obtain W where "W∈𝔅" and "W⊆converse(U)"
using uniformity_base_props(3) by blast
with ‹U∈?Φ› have "converse(U) ∈ ?Φ" unfolding Supersets_def
by auto
ultimately have "id(X)⊆U ∧ (∃V∈?Φ. V O V ⊆ U) ∧ converse(U)∈?Φ"
by simp
} thus ?thesis by simp
qed
ultimately show ?thesis unfolding IsUniformity_def by simp
qed
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} ∅"
shows "¬(Supersets(∅×∅,𝔅) {is a uniformity on} ∅)"
proof -
{ let ?Φ = "Supersets(∅×∅,𝔅)"
assume "?Φ {is a uniformity on} ∅"
from assms have "𝔅={∅}" using uniformity_base_props(5,6) by force
with ‹?Φ {is a uniformity on} ∅› have False
using supersets_in_empty unif_filter unfolding IsFilter_def by auto
} thus ?thesis by auto
qed
subsection‹Least upper bound of a set of uniformities›
text‹Uniformities on a set $X$ are naturally ordered by the inclusion relation.
Specifically, for two uniformities $\mathcal{U}_1$ and $\mathcal{U}_2$ on a set $X$
if $\mathcal{U}_1 \subseteq \mathcal{U}_2$ we say that $\mathcal{U}_2$ is finer than
$\mathcal{U}_1$ or that $\mathcal{U}_1$ is coarser than $\mathcal{U}_2$.
Turns out this order is complete: every nonempty set of uniformities has
a least upper bound, i.e. a supremum. ›
text‹We define ‹Uniformities(X)› as the set of all uniformities on $X$. ›
definition
"Uniformities(X) ≡ {Φ ∈ Pow(Pow(X×X)). Φ {is a uniformity on} X}"
text‹If $\Phi$ is a uniformity on $X$, then $\Phi$ is a collection of subsets of $X\times X$,
hence it's a member of ‹Uniformities(X)›.›
lemma unif_in_unifs: assumes "Φ {is a uniformity on} X"
shows "Φ ∈ Uniformities(X)"
using assms unfolding Uniformities_def IsUniformity_def IsFilter_def
by auto
text‹For nonempty sets the set of uniformities is not empty as well.›
lemma unifomities_exist: assumes "X≠∅" shows "Uniformities(X)≠∅"
unfolding Uniformities_def using assms min_uniformity by auto
text‹Uniformities on a set $X$ are naturally ordered by inclusion, we call
the resulting order relation ‹OrderOnUniformities›.›
definition
"OrderOnUniformities(X) ≡ InclusionOn(Uniformities(X))"
text‹The order defined by inclusion on uniformities is a partial order.›
lemma ord_unif_partial_ord:
shows "IsPartOrder(Uniformities(X),OrderOnUniformities(X))"
unfolding OrderOnUniformities_def using incl_is_partorder by simp
text‹In particular, the order defined by inclusion on uniformities is antisymmetric.
Having this as a separate fact is handy as we reference some lemmas
proven for antisymmetric (not necessarily partial order) relations.›
lemma ord_unif_antisymm: shows "antisym(OrderOnUniformities(X))"
using ord_unif_partial_ord unfolding IsPartOrder_def by simp
text‹If $X$ is not empty then the singleton $\{ X\times X\}$ is the minimal
element of the set of uniformities on $X$ ordered by inclusion
and the collection of subsets of $X\times X$ that contain the diagonal
is the maximal element.›
theorem uniformities_min_max: assumes "X≠∅" shows
"HasAminimum(OrderOnUniformities(X),Uniformities(X))"
"Minimum(OrderOnUniformities(X),Uniformities(X)) = {X×X}"
"HasAmaximum(OrderOnUniformities(X),Uniformities(X))"
"Maximum(OrderOnUniformities(X),Uniformities(X)) = {U∈Pow(X×X). id(X)⊆U}"
proof -
let ?𝔘 = "Uniformities(X)"
let ?r = "OrderOnUniformities(X)"
let ?M = "{U∈Pow(X×X). id(X)⊆U}"
from assms have "{X×X} ∈ ?𝔘" and "?M∈?𝔘"
unfolding Uniformities_def using min_uniformity max_uniformity
by auto
{ fix Φ assume "Φ ∈ ?𝔘"
then have "Φ {is a filter on} (X×X)"
unfolding Uniformities_def using unif_filter by simp
with ‹{X×X}∈?𝔘› ‹Φ∈?𝔘› have "⟨{X×X},Φ⟩ ∈ ?r"
unfolding IsFilter_def OrderOnUniformities_def InclusionOn_def
by simp
} with ‹{X×X} ∈ ?𝔘› show "HasAminimum(?r,?𝔘)" and "Minimum(?r,?𝔘) = {X×X}"
unfolding HasAminimum_def using Order_ZF_4_L15 ord_unif_antisymm
by auto
{ fix Φ assume "Φ ∈ ?𝔘"
then have "Φ ⊆ ?M" unfolding IsUniformity_def Uniformities_def
by auto
with ‹?M∈?𝔘› ‹Φ∈?𝔘› have "⟨Φ,?M⟩ ∈ ?r"
unfolding OrderOnUniformities_def InclusionOn_def by simp
} with ‹?M∈?𝔘› show "HasAmaximum(?r,?𝔘)" and "Maximum(?r,?𝔘) = ?M"
unfolding HasAmaximum_def using Order_ZF_4_L14 ord_unif_antisymm
by auto
qed
text‹Given a set of uniformities $\mathcal{U}$ on $X$ we define a collection of subsets of $X$
called ‹LUB_UnifBase› (the least upper bound base in comments)
as the set of all products of nonempty finite subsets of $\bigcup\mathcal{U}$.
The "least upper bound base" term is not justified at this point, but we will show later
that this set is actually a uniform base (i.e. a fundamental system of entourages)
on $X$ and hence the supersets of it form a uniformity on $X$, which is the supremum
(i.e. the least upper bound) of $\mathcal{U}$.›
definition "LUB_UnifBase(𝒰) = {⋂M. M ∈ FinPow(⋃𝒰)∖{∅}}"
text‹For any two sets in the least upper bound base there is a third one contained in both.›
lemma lub_unif_base_1st_cond:
assumes "𝒰⊆Uniformities(X)" "U⇩1 ∈ LUB_UnifBase(𝒰)" "U⇩2 ∈ LUB_UnifBase(𝒰)"
shows "∃U⇩3∈LUB_UnifBase(𝒰). U⇩3⊆U⇩1∩U⇩2"
proof -
let ?ℱ = "FinPow(⋃𝒰)∖{∅}"
from assms(2,3) obtain M⇩1 M⇩2 where
"M⇩1∈?ℱ" "M⇩1≠∅" "U⇩1=⋂M⇩1" "M⇩2∈?ℱ" "M⇩2≠∅" "U⇩2=⋂M⇩2"
unfolding LUB_UnifBase_def by auto
let ?M⇩3 = "M⇩1∪M⇩2"
from ‹M⇩1≠∅› ‹M⇩2≠∅› ‹U⇩1=⋂M⇩1› ‹U⇩2=⋂M⇩2› have "⋂?M⇩3 ⊆ U⇩1∩U⇩2"
by auto
with ‹M⇩1 ∈ ?ℱ› ‹M⇩2 ∈ ?ℱ› ‹U⇩2=⋂M⇩2› show ?thesis
using union_finpow unfolding LUB_UnifBase_def by auto
qed
text‹Each set in the least upper bound base contains the diagonal of $X\times X$.›
lemma lub_unif_base_2nd_cond:
assumes "𝒰⊆Uniformities(X)" "U ∈ LUB_UnifBase(𝒰)"
shows "id(X)⊆U"
using assms
unfolding LUB_UnifBase_def FinPow_def Uniformities_def IsUniformity_def
by blast
text‹The converse of each set from the least upper bound base contains a
set from it.›
lemma lub_unif_base_3rd_cond:
assumes "𝒰⊆Uniformities(X)" "U⇩1 ∈ LUB_UnifBase(𝒰)"
shows "∃U⇩2 ∈ LUB_UnifBase(𝒰). U⇩2 ⊆ converse(U⇩1)"
proof -
let ?ℱ = "FinPow(⋃𝒰)∖{∅}"
from assms(2) obtain M⇩1 where "M⇩1∈?ℱ" "M⇩1≠∅" "U⇩1=⋂M⇩1"
unfolding LUB_UnifBase_def by auto
let ?M⇩2 = "{converse(V). V∈M⇩1}"
from assms(1) ‹M⇩1∈?ℱ› have "∀V∈M⇩1. converse(V) ∈ ⋃𝒰"
unfolding FinPow_def Uniformities_def using entourage_props(4)
by blast
with ‹M⇩1∈?ℱ› have "⋂?M⇩2 ∈ LUB_UnifBase(𝒰)"
using fin_image_fin0 unfolding LUB_UnifBase_def by auto
from assms(1) ‹M⇩1∈?ℱ› ‹U⇩1=⋂M⇩1› have "⋂?M⇩2 ⊆ converse(U⇩1)"
unfolding Uniformities_def FinPow_def using prod_converse
by blast
with ‹⋂?M⇩2 ∈ LUB_UnifBase(𝒰)› show ?thesis by auto
qed
text‹For each set (relation) $U_1$ from the least upper bound base there is another one $U_2$
such that $U_2$ composed with itself is contained in $U_1$.›
lemma lub_unif_base_4th_cond:
assumes "𝒰⊆Uniformities(X)" "U⇩1 ∈ LUB_UnifBase(𝒰)"
shows "∃U⇩2 ∈ LUB_UnifBase(𝒰). U⇩2 O U⇩2 ⊆ U⇩1"
proof -
let ?ℱ = "FinPow(⋃𝒰)∖{∅}"
from assms(2) obtain M⇩1 where "M⇩1∈?ℱ" "M⇩1≠∅" "U⇩1=⋂M⇩1"
unfolding LUB_UnifBase_def by auto
from ‹M⇩1∈?ℱ› have "Finite(M⇩1)" unfolding FinPow_def by simp
{ fix V assume "V∈M⇩1"
with assms(1) ‹M⇩1∈?ℱ› obtain Φ where "Φ∈𝒰" and "V∈Φ"
unfolding FinPow_def by auto
with assms(1) ‹V∈Φ› obtain W where "W∈Φ" and "W O W ⊆ V"
unfolding Uniformities_def using entourage_props(3) by blast
with ‹Φ∈𝒰› have "∃W∈⋃𝒰. W O W ⊆ V" by auto
} hence "∀V∈M⇩1. ∃W∈⋃𝒰. W O W ⊆ V" by simp
with ‹Finite(M⇩1)› have "∃f∈M⇩1→⋃𝒰. ∀V∈M⇩1. f`(V) O f`(V) ⊆ V"
by (rule finite_choice_fun)
then obtain f where "f:M⇩1→⋃𝒰" and "∀V∈M⇩1. f`(V) O f`(V) ⊆ V"
by auto
let ?M⇩2 = "{f`(V). V∈M⇩1}"
from ‹f:M⇩1→⋃𝒰› have "∀V∈M⇩1. f`(V) ∈ ⋃𝒰" using apply_funtype by blast
with ‹M⇩1∈?ℱ› have "⋂?M⇩2 ∈ LUB_UnifBase(𝒰)"
using fin_image_fin0 unfolding LUB_UnifBase_def by auto
from ‹M⇩1≠∅› ‹∀V∈M⇩1. f`(V) O f`(V) ⊆ V› have
"(⋂V∈M⇩1. f`(V)) O (⋂V∈M⇩1. f`(V)) ⊆ (⋂V∈M⇩1. V)"
by (rule square_incl_product)
with ‹U⇩1=⋂M⇩1› ‹⋂?M⇩2 ∈ LUB_UnifBase(𝒰)› show ?thesis by auto
qed
text‹The least upper bound base is a collection of relations on $X$.›
lemma lub_unif_base_5th_cond:
assumes "𝒰⊆Uniformities(X)" shows "LUB_UnifBase(𝒰) ⊆ Pow(X×X)"
using assms unfolding Uniformities_def FinPow_def LUB_UnifBase_def
by blast
text‹If a collection of uniformities is nonempty, then the least upper bound base
is non-empty as well.›
lemma lub_unif_base_6th_cond: assumes "𝒰⊆Uniformities(X)" "𝒰≠∅"
shows "LUB_UnifBase(𝒰) ≠ ∅"
proof -
from assms(2) obtain Φ where "Φ∈𝒰" by auto
with assms(1) have "⋃𝒰 ≠ ∅" unfolding Uniformities_def
using uniformity_non_empty by blast
then show "LUB_UnifBase(𝒰) ≠ ∅" using finpow_nempty_nempty
unfolding LUB_UnifBase_def by simp
qed
text‹If a collection of uniformities $\mathcal{U}$ is nonempty, $\mathcal{B}$
denotes the least upper bound base for $\mathcal{U}$, then $\mathcal{B}$
is a uniform base on $X$, hence its supersets form a uniformity on $X$ and
the uniform topology generated by that uniformity is indeed a topology on $X$. ›
theorem lub_unif_base_base:
assumes "X≠∅" "𝒰⊆Uniformities(X)" "𝒰≠∅"
defines "𝔅 ≡ LUB_UnifBase(𝒰)"
shows
"𝔅 {is a uniform base on} X"
"Supersets(X×X,𝔅) {is a uniformity on} X"
"UniformTopology(Supersets(X×X,𝔅),X) {is a topology}"
"⋃UniformTopology(Supersets(X×X,𝔅),X) = X"
using assms lub_unif_base_1st_cond lub_unif_base_2nd_cond
lub_unif_base_3rd_cond lub_unif_base_4th_cond lub_unif_base_5th_cond
lub_unif_base_6th_cond uniformity_base_is_base uniform_top_is_top
unfolding IsUniformityBaseOn_def by simp_all
text‹At this point we know that supersets with respect to $X\times X$
of the least upper bound base for a collection of uniformities $\mathcal{U}$ form a uniformity.
To shorten the notation we will call this uniformity ‹LUB_Unif(X,𝒰)›.›
definition
"LUB_Unif(X,𝒰) ≡ Supersets(X×X,LUB_UnifBase(𝒰))"
text‹For any collection of uniformities $\mathcal{U}$ on a nonempty set $X$
the ‹LUB_Unif(X,𝒰)› collection defined above is indeed an upper bound of $\mathcal{U}$
in the order defined by the inclusion relation.›
lemma lub_unif_upper_bound:
assumes "X≠∅" "𝒰⊆Uniformities(X)" "Φ∈𝒰"
shows "⟨Φ,LUB_Unif(X,𝒰)⟩ ∈ OrderOnUniformities(X)"
proof -
let ?Ψ = "LUB_Unif(X,𝒰)"
from assms have "?Ψ ∈ Uniformities(X)"
unfolding LUB_Unif_def using lub_unif_base_base(2) unif_in_unifs
by blast
from assms(2,3) have
"Φ ∈ Uniformities(X)" and "Φ {is a uniformity on} X"
unfolding Uniformities_def by auto
{ fix E assume "E∈Φ"
with assms(3) have "E ∈ LUB_UnifBase(𝒰)"
using singleton_in_finpow unfolding LUB_UnifBase_def
by blast
with ‹Φ {is a uniformity on} X› ‹E∈Φ› have "E ∈ ?Ψ"
using entourage_props(1) superset_gen unfolding LUB_Unif_def
by simp
} hence "Φ ⊆ ?Ψ" by auto
with ‹Φ ∈ Uniformities(X)› ‹?Ψ ∈ Uniformities(X)› show ?thesis
unfolding OrderOnUniformities_def InclusionOn_def by simp
qed
text‹Any upper bound (in the order defined by inclusion relation) of a nonempty collection of
uniformities $\mathcal{U}$ on a nonempty set $X$ is greater or equal (in that order)
than ‹LUB_Unif(X,𝒰)›. Together with ‹lub_unif_upper_bound› it means that ‹LUB_Unif(X,𝒰)›
is indeed the least upper bound of $\mathcal{U}$.›
lemma lub_unif_lub:
assumes "X≠∅" "𝒰⊆Uniformities(X)" "𝒰≠∅" and
"∀Φ∈𝒰. ⟨Φ,Ψ⟩ ∈ OrderOnUniformities(X)"
shows "⟨LUB_Unif(X,𝒰),Ψ⟩ ∈ OrderOnUniformities(X)"
proof -
from assms(3,4) have "Ψ ∈ Uniformities(X)"
unfolding OrderOnUniformities_def InclusionOn_def by auto
then have "Ψ {is a filter on} (X×X)"
unfolding Uniformities_def IsUniformity_def by simp
from assms(4) have "FinPow(⋃𝒰)∖{∅} ⊆ FinPow(Ψ)∖{∅}"
unfolding OrderOnUniformities_def InclusionOn_def FinPow_def
by auto
with ‹Ψ {is a filter on} (X×X)› have "LUB_UnifBase(𝒰) ⊆ Ψ"
using filter_fin_inter_closed unfolding LUB_UnifBase_def by auto
with ‹Ψ {is a filter on} (X×X)› have "LUB_Unif(X,𝒰) ⊆ Ψ"
using filter_superset_closed unfolding LUB_Unif_def by simp
with assms(1,2,3) ‹Ψ ∈ Uniformities(X)› show ?thesis
using lub_unif_base_base(2) unif_in_unifs
unfolding LUB_Unif_def OrderOnUniformities_def InclusionOn_def
by simp
qed
text‹A nonempty collection $\mathcal{U}$ of uniformities on $X$ has a supremum
(i.e. the least upper bound).›
lemma lub_unif_sup: assumes "X≠∅" "𝒰⊆Uniformities(X)" "𝒰≠∅"
shows "HasAsupremum(OrderOnUniformities(X),𝒰)" and
"LUB_Unif(X,𝒰) = Supremum(OrderOnUniformities(X),𝒰)"
proof -
let ?r = "OrderOnUniformities(X)"
let ?S = "LUB_Unif(X,𝒰)"
from assms(1,2) have "antisym(?r)" and "∀Φ∈𝒰. ⟨Φ,?S⟩ ∈ ?r"
using ord_unif_antisymm lub_unif_upper_bound by simp_all
from assms have I: "∀Ψ. (∀Φ∈𝒰. ⟨Φ,Ψ⟩ ∈ ?r) ⟶ ⟨?S,Ψ⟩ ∈ ?r"
using lub_unif_lub by simp
with assms(3) ‹antisym(?r)› ‹∀Φ∈𝒰. ⟨Φ,?S⟩ ∈ ?r› show "HasAsupremum(?r,𝒰)"
unfolding HasAsupremum_def using Order_ZF_5_L5(1) by blast
from assms(3) ‹antisym(?r)› ‹∀Φ∈𝒰. ⟨Φ,?S⟩ ∈ ?r› I
show "?S = Supremum(?r,𝒰)" using Order_ZF_5_L5(2) by blast
qed
text‹The order on uniformities derived from inclusion is complete.›
theorem uniformities_complete: assumes "X≠∅"
shows "OrderOnUniformities(X) {is complete}"
proof -
let ?r = "OrderOnUniformities(X)"
{ fix 𝒰 assume "𝒰≠∅" and "IsBoundedAbove(𝒰,?r)"
then obtain Ψ where "∀Φ∈𝒰. ⟨Φ,Ψ⟩ ∈ ?r"
unfolding IsBoundedAbove_def by auto
then have "𝒰⊆Uniformities(X)"
unfolding OrderOnUniformities_def InclusionOn_def by auto
with assms ‹𝒰≠∅› have "HasAsupremum(?r,𝒰)"
using lub_unif_sup by simp
}
then show "?r {is complete}" unfolding HasAsupremum_def IsComplete_def
by simp
qed
end