section ‹ Uniform spaces ›
theory UniformSpace_ZF imports Topology_ZF_4a
begin
text‹ This theory defines uniform spaces and proves their basic properties. ›
subsection‹ Definition and motivation ›
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‹ 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" "V∈Φ" and "x∈X"
shows "V``{x} ≠ 0" and "x ∈ V``{x}"
proof -
from assms(1,2) have "id(X) ⊆ V" using IsUniformity_def IsFilter_def
by auto
with ‹x∈X› show" x∈V``{x}" and "V``{x} ≠ 0" by auto
qed
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 "0 ∉ ℳ`(x)"
proof -
from assms ‹x∈X› have "0 ∉ {V``{x}.V∈Φ}" using neigh_not_empty by blast
with ‹ℳ`(x) = {V``{x}.V∈Φ}› show "0 ∉ ℳ`(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‹ 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(Φ)›. The definition may be a bit
cryptic but it just combines the construction of a neighborhood system from uniformity as in
the assumptions of lemma ‹filter_from_uniformity› and the construction of topology from
a neighborhood system from theorem ‹topology_from_neighs›.
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 ∈ {⟨t,{V``{t}.V∈Φ}⟩.t∈X}`(x)}"
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 UniformTopology_def topology_from_neighs
by auto
end