Theory UniformSpace_ZF_2
section ‹ Alternative definitions of uniformity ›
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 alternative definitions based of the
notion of uniform covers and pseudometrics.
›
subsection‹ Uniform covers ›
text‹ Given a set $X$ we can consider collections of subsets of $X$ whose unions are equal to $X$.
Any such collection is called a cover of $X$. We can define relation on the set of covers
of $X$, called "star refinement" (definition below). A collection of covers is a
"family of uniform covers" if it is a filter with respect to the start refinement ordering.
A member of such family is called a "uniform cover", but one has to remember that this notion
has meaning only in the contexts a the whole family of uniform covers. Looking at a specific cover
in isolation we can not say whether it is a uniform cover or not. ›
text‹ The set of all covers of $X$ is called ‹Covers(X)›. ›
definition
"Covers(X) ≡ {P ∈ Pow(Pow(X)). ⋃P = X}"
text‹A cover of a nonempty set must have a nonempty member.›
lemma cover_nonempty: assumes "X≠0" "P ∈ Covers(X)"
shows "∃U∈P. U≠0"
using assms unfolding Covers_def by blast
text‹ A "star" of $R$ with respect to $\mathcal{R}$ is the union of all $S\in \mathcal{R}$ that
intersect $R$. ›
definition
"Star(R,ℛ) ≡ ⋃{S∈ℛ. S∩R ≠ 0}"
text‹An element of $\mathcal{R}$ is a subset of its star with respect to $\mathcal{R}$. ›
lemma element_subset_star: assumes "U∈P" shows "U ⊆ Star(U,P)"
using assms unfolding Star_def by auto
text‹An alternative formula for star of a singleton.›
lemma star_singleton: shows "(⋃{V×V. V∈P})``{x} = Star({x},P)"
unfolding Star_def by blast
text‹Star of a larger set is larger.›
lemma star_mono: assumes "U⊆V" shows "Star(U,P) ⊆ Star(V,P)"
using assms unfolding Star_def by blast
text‹In particular, star of a set is larger than star of any singleton in that set.›
corollary star_single_mono: assumes "x∈U" shows "Star({x},P) ⊆ Star(U,P)"
using assms star_mono by auto
text‹A cover $\mathcal{R}$ (of $X$) is said to be a "barycentric refinement" of a cover $\mathcal{C}$
iff for every $x\in X$ the star of $\{x\}$ in $\mathcal{R}$ is contained
in some $C\in \mathcal{C}$. ›
definition
IsBarycentricRefinement ("_ <⇧B _" 90)
where "P <⇧B Q ≡ ∀x∈⋃P.∃U∈Q. Star({x},P) ⊆ U"
text‹A cover is a barycentric refinement of the collection of stars of the singletons
$\{x \}$ as $x$ ranges over $X$.›
lemma singl_star_bary:
assumes "P ∈ Covers(X)" shows "P <⇧B {Star({x},P). x∈X}"
using assms unfolding Covers_def IsBarycentricRefinement_def by blast
text‹ A cover $\mathcal{R}$ is a "star refinement" of a cover $\mathcal{C}$ iff
for each $R\in \mathcal{R}$ there is a $C\in \mathcal{C}$ such that the star of $R$ with
respect to $\mathcal{R}$ is contained in $C$. ›
definition
IsStarRefinement ("_ <⇧* _" 90)
where "P <⇧* Q ≡ ∀U∈P.∃V∈Q. Star(U,P) ⊆ V"
text‹Every cover star-refines the trivial cover $\{ X\}$. ›
lemma cover_stref_triv: assumes "P ∈ Covers(X)" shows "P <⇧* {X}"
using assms unfolding Star_def IsStarRefinement_def Covers_def by auto
text‹Star refinement implies barycentric refinement. ›
lemma star_is_bary: assumes "Q∈Covers(X)" and "Q <⇧* P"
shows "Q <⇧B P"
proof -
from assms(1) have "⋃Q = X" unfolding Covers_def by simp
{ fix x assume "x∈X"
with ‹⋃Q = X› obtain R where "R∈Q" and "x∈R" by auto
with assms(2) obtain U where "U∈P" and "Star(R,Q) ⊆ U"
unfolding IsStarRefinement_def by auto
from ‹x∈R› ‹Star(R,Q) ⊆ U› have "Star({x},Q) ⊆ U"
using star_single_mono by blast
with ‹U∈P› have "∃U∈P. Star({x},Q) ⊆ U" by auto
} with ‹⋃Q = X› show ?thesis unfolding IsBarycentricRefinement_def
by simp
qed
text‹ Barycentric refinement of a barycentric refinement is a star refinement. ›
lemma bary_bary_star:
assumes "P∈Covers(X)" "Q∈Covers(X)" "R∈Covers(X)" "P <⇧B Q" "Q <⇧B R" "X≠0"
shows "P <⇧* R"
proof -
{ fix U assume "U∈P"
{ assume "U = 0"
then have "Star(U,P) = 0" unfolding Star_def by simp
from assms(6,3) obtain V where "V∈R" using cover_nonempty by auto
with ‹Star(U,P) = 0› have "∃V∈R. Star(U,P) ⊆ V" by auto
}
moreover
{ assume "U≠0"
then obtain x⇩0 where "x⇩0∈U" by auto
with assms(1,2,5) ‹U∈P› obtain V where "V∈R" and "Star({x⇩0},Q) ⊆ V"
unfolding Covers_def IsBarycentricRefinement_def by auto
have "Star(U,P) ⊆ V"
proof -
{ fix W assume "W∈P" and "W∩U ≠ 0"
from ‹W∩U ≠ 0› obtain x where "x∈W∩U" by auto
with assms(2) ‹U∈P› have "x∈⋃P" by auto
with assms(4) obtain C where "C∈Q" and "Star({x},P) ⊆ C"
unfolding IsBarycentricRefinement_def by blast
with ‹U∈P› ‹W∈P› ‹x∈W∩U› ‹x⇩0∈U› ‹Star({x⇩0},Q) ⊆ V› have "W⊆V"
unfolding Star_def by blast
} then show "Star(U,P) ⊆ V" unfolding Star_def by auto
qed
with ‹V∈R› have "∃V∈R. Star(U,P) ⊆ V" by auto
}
ultimately have "∃V∈R. Star(U,P) ⊆ V" by auto
} then show "P <⇧* R" unfolding IsStarRefinement_def by simp
qed
text‹The notion of a filter defined in ‹Topology_ZF_4› is not sufficiently general to use it to
define uniform covers, so we write the conditions directly. A nonempty
collection $\Theta$ of covers of $X$ is a family of uniform covers if
a) if $\mathcal{R} \in \Theta$ and $\mathcal{C}$ is any cover of $X$ such that $\mathcal{R}$ is
a star refinement of $\mathcal{C}$, then $\mathcal{C} \in \Theta$.
b) For any $\mathcal{C},\mathcal{D} \in \Theta$ there is some $\mathcal{R}\in\Theta$
such that $\mathcal{R}$ is a star refinement of both $\mathcal{C}$ and $\mathcal{R}$.
This departs slightly from the definition in Wikipedia that requires that $\Theta$ contains the
trivial cover $\{ X\}$. As we show in lemma ‹unicov_contains_trivial› below we don't loose
anything by weakening the definition this way.
›
definition
AreUniformCovers ("_ {are uniform covers of} _" 90)
where "Θ {are uniform covers of} X ≡ Θ ⊆ Covers(X) ∧ Θ≠0 ∧
(∀ℛ∈Θ.∀𝒞∈Covers(X). ((ℛ <⇧* 𝒞) ⟶ 𝒞∈Θ)) ∧
(∀𝒞∈Θ.∀𝒟∈Θ.∃ℛ∈Θ.(ℛ <⇧* 𝒞) ∧ (ℛ <⇧* 𝒟))"
text‹A family of uniform covers contain the trivial cover $\{ X\}$.›
lemma unicov_contains_triv: assumes "Θ {are uniform covers of} X"
shows "{X} ∈ Θ"
proof -
from assms obtain ℛ where "ℛ∈Θ" unfolding AreUniformCovers_def by blast
with assms show ?thesis using cover_stref_triv
unfolding AreUniformCovers_def Covers_def by auto
qed
text‹If $\Theta$ are uniform covers of $X$ then we can recover $X$ from $\Theta$ by taking
$\bigcup\bigcup \Theta$. ›
lemma space_from_unicov: assumes "Θ {are uniform covers of} X" shows "X = ⋃⋃Θ"
proof
from assms show "X ⊆ ⋃⋃Θ" using unicov_contains_triv
unfolding AreUniformCovers_def by auto
from assms show "⋃⋃Θ ⊆ X" unfolding AreUniformCovers_def Covers_def
by auto
qed
text‹ Every uniform cover has a star refinement. ›
lemma unicov_has_star_ref:
assumes "Θ {are uniform covers of} X" and "P∈Θ"
shows "∃Q∈Θ. (Q <⇧* P)"
using assms unfolding AreUniformCovers_def by blast
text‹ In particular, every uniform cover has a barycentric refinement. ›
corollary unicov_has_bar_ref:
assumes "Θ {are uniform covers of} X" and "P∈Θ"
shows "∃Q∈Θ. (Q <⇧B P)"
proof -
from assms obtain Q where "Q∈Θ" and "Q <⇧* P"
using unicov_has_star_ref by blast
with assms show ?thesis
unfolding AreUniformCovers_def using star_is_bary by blast
qed
text‹ From the definition of uniform covers we know that if a uniform cover $P$
is a star-refinement of a cover $Q$ then $Q$ is in a uniform cover. The next lemma
shows that in order for $Q$ to be a uniform cover it is sufficient that $P$ is a
barycentric refinement of $Q$. ›
lemma unicov_bary_cov:
assumes "Θ {are uniform covers of} X" "P∈Θ" "Q ∈ Covers(X)" "P <⇧B Q" and "X≠0"
shows "Q∈Θ"
proof -
from assms(1,2) obtain R where "R∈Θ" and "R <⇧B P"
using unicov_has_bar_ref by blast
from assms(1,2,3) ‹R∈Θ› have
"P ∈ Covers(X)" "Q ∈ Covers(X)" "R ∈ Covers(X)"
unfolding AreUniformCovers_def by auto
with assms(1,3,4,5) ‹R∈Θ› ‹R <⇧B P› show ?thesis
using bary_bary_star unfolding AreUniformCovers_def by auto
qed
text‹ A technical lemma to simplify proof of the ‹uniformity_from_unicov› theorem. ›
lemma star_ref_mem: assumes "U∈P" "P<⇧*Q" and "⋃{W×W. W∈Q} ⊆ A"
shows "U×U ⊆ A"
proof -
from assms(1,2) obtain W where "W∈Q" and "⋃{S∈P. S∩U ≠ 0} ⊆ W"
unfolding IsStarRefinement_def Star_def by auto
with assms(1,3) show "U×U ⊆ A" by blast
qed
text‹An identity related to square (in the sense of composition) of a relation of the
form $\bigcup \{U\times U : U\in P\}$.
I am amazed that Isabelle can see that this is true without an explicit proof, I can't. ›
lemma rel_square_starr: shows
"(⋃{U×U. U∈P}) O (⋃{U×U. U∈P}) = ⋃{U×Star(U,P). U∈P}"
unfolding Star_def by blast
text‹ An identity similar to ‹rel_square_starr› but with ‹Star› on the left side of the Cartesian
product: ›
lemma rel_square_starl: shows
"(⋃{U×U. U∈P}) O (⋃{U×U. U∈P}) = ⋃{Star(U,P)×U. U∈P}"
unfolding Star_def by blast
text‹A somewhat technical identity about the square of a symmetric relation: ›
lemma rel_sq_image:
assumes "W = converse(W)" "domain(W) ⊆ X"
shows "Star({x},{W``{t}. t∈X}) = (W O W)``{x}"
proof
have I: "Star({x},{W``{t}. t∈X}) = ⋃{S∈{W``{t}. t∈X}. x∈S}"
unfolding Star_def by auto
{ fix y assume "y ∈ Star({x},{W``{t}. t∈X})"
with I obtain S where "y∈S" "x∈S" "S ∈ {W``{t}. t∈X}" by auto
from ‹S ∈ {W``{t}. t∈X}› obtain t where "t∈X" and "S = W``{t}"
by auto
with ‹x∈S› ‹y∈S› have "⟨t,x⟩ ∈ W" and "⟨t,y⟩ ∈ W"
by auto
from ‹⟨t,x⟩ ∈ W› have "⟨x,t⟩ ∈ converse(W)" by auto
with assms(1) ‹⟨t,y⟩ ∈ W› have "y ∈ (W O W)``{x}"
using rel_compdef by auto
} then show "Star({x},{W``{t}. t∈X}) ⊆ (W O W)``{x}"
by blast
{ fix y assume "y∈(W O W)``{x}"
then obtain t where "⟨x,t⟩ ∈ W" and "⟨t,y⟩ ∈ W"
using rel_compdef by auto
from assms(2) ‹⟨t,y⟩ ∈ W› have "t∈X" by auto
from ‹⟨x,t⟩ ∈ W› have "⟨t,x⟩ ∈ converse(W)" by auto
with assms(1) I ‹⟨t,y⟩ ∈ W› ‹t∈X› have "y ∈ Star({x},{W``{t}. t∈X})"
by auto
} then show "(W O W)``{x} ⊆ Star({x},{W``{t}. t∈X})"
by blast
qed
text‹ Given a family of uniform covers of $X$ we can create a uniformity on $X$ by taking the supersets
of $\bigcup \{A\times A: A\in P \}$ as $P$ ranges over the uniform covers. The next definition
specifies the operation creating entourages from uniform covers. ›
definition
"UniformityFromUniCov(X,Θ) ≡ Supersets(X×X,{⋃{U×U. U∈P}. P∈Θ})"
text‹For any member $P$ of a cover $\Theta$ the set $\bigcup \{U\times U : U\in P\}$
is a member of ‹UniformityFromUniCov(X,Θ)›. ›
lemma basic_unif: assumes "Θ ⊆ Covers(X)" "P∈Θ"
shows "⋃{U×U. U∈P} ∈ UniformityFromUniCov(X,Θ)"
using assms unfolding UniformityFromUniCov_def Supersets_def Covers_def
by blast
text‹If $\Theta$ is a family of uniform covers of $X$ then
‹UniformityFromUniCov(X,Θ)› is a uniformity on $X$ ›
theorem uniformity_from_unicov:
assumes "Θ {are uniform covers of} X" "X≠0"
shows "UniformityFromUniCov(X,Θ) {is a uniformity on} X"
proof -
let ?Φ = "UniformityFromUniCov(X,Θ)"
have "?Φ {is a filter on} (X×X)"
proof -
have "0 ∉ ?Φ"
proof -
{ assume "0 ∈ ?Φ"
then obtain P where "P∈Θ" and "0 = ⋃{U×U. U∈P}"
unfolding UniformityFromUniCov_def Supersets_def by auto
hence "⋃P = 0" by auto
with assms ‹P∈Θ› have False unfolding AreUniformCovers_def Covers_def
by auto
} thus ?thesis by auto
qed
moreover have "X×X ∈ ?Φ"
proof -
from assms have "X×X ∈ {⋃{U×U. U∈P}. P∈Θ}"
using unicov_contains_triv unfolding AreUniformCovers_def
by auto
then show ?thesis unfolding Supersets_def UniformityFromUniCov_def
by blast
qed
moreover have "?Φ ⊆ Pow(X×X)"
unfolding UniformityFromUniCov_def Supersets_def by auto
moreover have "∀A∈?Φ.∀B∈?Φ. A∩B ∈ ?Φ"
proof -
{ fix A B assume "A∈?Φ" "B∈?Φ"
then have "A∩B ⊆ X×X" unfolding UniformityFromUniCov_def Supersets_def
by auto
from ‹A∈?Φ› ‹B∈?Φ› obtain P⇩A P⇩B where
"P⇩A∈Θ" "P⇩B∈Θ" and I:"⋃{U×U. U∈P⇩A} ⊆ A" "⋃{U×U. U∈P⇩B} ⊆ B"
unfolding UniformityFromUniCov_def Supersets_def by auto
from assms(1) ‹P⇩A∈Θ› ‹P⇩B∈Θ› obtain P
where "P∈Θ" and "P<⇧*P⇩A" and "P<⇧*P⇩B"
unfolding AreUniformCovers_def by blast
have "⋃{U×U. U∈P} ⊆ A∩B"
proof -
{ fix U assume "U∈P"
with ‹P<⇧*P⇩A› ‹P<⇧*P⇩B› I have "U×U ⊆ A" and "U×U ⊆ B"
using star_ref_mem by auto
} thus ?thesis by blast
qed
with ‹A∩B ⊆ X×X› ‹P∈Θ› have "A∩B ∈ ?Φ"
unfolding Supersets_def UniformityFromUniCov_def by auto
} thus ?thesis by auto
qed
moreover have
"∀B∈?Φ.∀C∈Pow(X×X). B⊆C ⟶ C∈?Φ"
proof -
{ fix B C assume "B∈?Φ" "C∈Pow(X×X)" "B⊆C"
from ‹B∈?Φ› obtain P⇩B where "⋃{U×U. U∈P⇩B} ⊆ B" "P⇩B∈Θ"
unfolding UniformityFromUniCov_def Supersets_def by auto
with ‹C∈Pow(X×X)› ‹B⊆C› have "C∈?Φ"
unfolding UniformityFromUniCov_def Supersets_def by blast
} thus ?thesis by auto
qed
ultimately show ?thesis unfolding IsFilter_def by simp
qed
moreover have "∀A∈?Φ. id(X) ⊆ A ∧ (∃B∈?Φ. B O B ⊆ A) ∧ converse(A) ∈ ?Φ"
proof
fix A assume "A∈?Φ"
then obtain P where "⋃{U×U. U∈P} ⊆ A" "P∈Θ"
unfolding UniformityFromUniCov_def Supersets_def by auto
have "id(X)⊆A"
proof -
from assms(1) ‹P∈Θ› have "⋃P = X" unfolding AreUniformCovers_def Covers_def
by auto
with ‹⋃{U×U. U∈P} ⊆ A› show ?thesis by auto
qed
moreover have "∃B∈?Φ. B O B ⊆ A"
proof -
from assms(1) ‹P∈Θ› have "⋃{U×U. U∈P} ∈ ?Φ"
unfolding AreUniformCovers_def Covers_def UniformityFromUniCov_def Supersets_def
by auto
from assms(1) ‹P∈Θ› obtain Q where "Q∈Θ" and "Q <⇧* P" using unicov_has_star_ref
by blast
let ?B = "⋃{U×U. U∈Q}"
from assms(1) ‹Q∈Θ› have "?B ∈ ?Φ"
unfolding AreUniformCovers_def Covers_def UniformityFromUniCov_def Supersets_def
by auto
moreover have "?B O ?B ⊆ A"
proof -
have II: "?B O ?B = ⋃{U×Star(U,Q). U∈Q}" using rel_square_starr
by simp
have "∀U∈Q. ∃V∈P. U×Star(U,Q) ⊆ V×V"
proof
fix U assume "U∈Q"
with ‹Q <⇧* P› obtain V where "V∈P" and "Star(U,Q) ⊆ V"
unfolding IsStarRefinement_def by blast
with ‹U∈Q› have "V∈P" and "U×Star(U,Q) ⊆ V×V" using element_subset_star
by auto
thus "∃V∈P. U×Star(U,Q) ⊆ V×V" by auto
qed
hence "⋃{U×Star(U,Q). U∈Q} ⊆ ⋃{V×V. V∈P}" by blast
with ‹⋃{V×V. V∈P} ⊆ A› have "⋃{U×Star(U,Q). U∈Q} ⊆ A" by blast
with II show ?thesis by simp
qed
ultimately show ?thesis by auto
qed
moreover from ‹A∈?Φ› ‹P∈Θ› ‹⋃{U×U. U∈P} ⊆ A› have "converse(A) ∈ ?Φ"
unfolding AreUniformCovers_def UniformityFromUniCov_def Supersets_def
by auto
ultimately show "id(X) ⊆ A ∧ (∃B∈?Φ. B O B ⊆ A) ∧ converse(A) ∈ ?Φ"
by simp
qed
ultimately show "?Φ {is a uniformity on} X" unfolding IsUniformity_def
by simp
qed
text‹Given a uniformity $\Phi$ on $X$ we can create a family of uniform covers by taking the
collection of covers $P$ for which there exist an entourage $U\in \Phi$ such that
for each $x\in X$, there is an $A\in P$ such that $U(\{ x\}) \subseteq A$. The next definition
specifies the operation of creating a family of uniform covers from a uniformity. ›
definition
"UniCovFromUniformity(X,Φ) ≡ {P∈Covers(X). ∃U∈Φ.∀x∈X.∃A∈P. U``({x}) ⊆ A}"
text‹When we convert the quantifiers into unions and intersections in the definition
of ‹UniCovFromUniformity› we get an alternative definition of the operation
that creates a family of uniform covers from a uniformity. Just a curiosity, not used anywhere.›
lemma UniCovFromUniformityDef: assumes "X≠0"
shows "UniCovFromUniformity(X,Φ) = (⋃U∈Φ.⋂x∈X. {P∈Covers(X). ∃A∈P. U``({x}) ⊆ A})"
proof -
have "{P∈Covers(X). ∃U∈Φ.∀x∈X.∃A∈P. U``({x}) ⊆ A} =
(⋃U∈Φ.⋂x∈X. {P∈Covers(X). ∃A∈P. U``({x}) ⊆ A})"
proof
{ fix P assume "P∈{P∈Covers(X). ∃U∈Φ.∀x∈X.∃A∈P. U``({x}) ⊆ A}"
then have "P∈Covers(X)" and "∃U∈Φ.∀x∈X.∃A∈P. U``({x}) ⊆ A" by auto
then obtain U where "U∈Φ" and "∀x∈X.∃A∈P. U``({x}) ⊆ A" by auto
with assms ‹P∈Covers(X)› have "P ∈ (⋂x∈X. {P∈Covers(X). ∃A∈P. U``({x}) ⊆ A})"
by auto
with ‹U∈Φ› have "P∈(⋃U∈Φ.⋂x∈X. {P∈Covers(X). ∃A∈P. U``({x}) ⊆ A})"
by blast
} then show
"{P∈Covers(X). ∃U∈Φ.∀x∈X.∃A∈P. U``({x}) ⊆ A} ⊆
(⋃U∈Φ.⋂x∈X. {P∈Covers(X). ∃A∈P. U``({x}) ⊆ A})"
using subset_iff by simp
{ fix P assume "P∈(⋃U∈Φ.⋂x∈X. {P∈Covers(X). ∃A∈P. U``({x}) ⊆ A})"
then obtain U where "U∈Φ" "P ∈ (⋂x∈X. {P∈Covers(X). ∃A∈P. U``({x}) ⊆ A})"
by auto
with assms have "P∈Covers(X)" and "∀x∈X.∃A∈P. U``({x}) ⊆ A" by auto
with ‹U∈Φ› have "P∈{P∈Covers(X). ∃U∈Φ.∀x∈X.∃A∈P. U``({x}) ⊆ A}"
by auto
} then show "(⋃U∈Φ.⋂x∈X. {P∈Covers(X). ∃A∈P. U``({x}) ⊆ A}) ⊆
{P∈Covers(X). ∃U∈Φ.∀x∈X.∃A∈P. U``({x}) ⊆ A}" by auto
qed
then show ?thesis unfolding UniCovFromUniformity_def by simp
qed
text‹If $\Phi$ is a (diagonal) uniformity on $X$, then covers of the form
$\{ W\{ x\} : x\in X\}$ are members of ‹UniCovFromUniformity(X,Φ)›. ›
lemma cover_image:
assumes "Φ {is a uniformity on} X" "W∈Φ"
shows "{W``{x}. x∈X} ∈ UniCovFromUniformity(X,Φ)"
proof -
let ?P = "{W``{x}. x∈X}"
have "?P ∈ Covers(X)"
proof -
from assms have "W ⊆ X×X" and "?P ∈ Pow(Pow(X))"
using entourage_props(1) by auto
moreover have "⋃?P = X"
proof
from ‹W ⊆ X×X› show "⋃?P ⊆ X" by auto
from assms show "X ⊆ ⋃?P" using neigh_not_empty(2) by auto
qed
ultimately show ?thesis unfolding Covers_def by simp
qed
moreover from assms(2) have "∃W∈Φ. ∀x∈X. ∃A∈?P. W``{x} ⊆ A"
by auto
ultimately show ?thesis unfolding UniCovFromUniformity_def
by simp
qed
text‹If $\Phi$ is a (diagonal) uniformity on $X$, then every two elements
of ‹UniCovFromUniformity(X,Φ)› have a common barycentric refinement.›
lemma common_bar_refinemnt:
assumes
"Φ {is a uniformity on} X"
"Θ = UniCovFromUniformity(X,Φ)"
"𝒞∈Θ" "𝒟∈Θ"
shows "∃ℛ∈Θ.(ℛ <⇧B 𝒞) ∧ (ℛ <⇧B 𝒟)"
proof -
from assms(2,3) obtain U where "U∈Φ" and I: "∀x∈X.∃C∈𝒞. U``{x} ⊆ C"
unfolding UniCovFromUniformity_def by auto
from assms(2,4) obtain V where "V∈Φ" and II: "∀x∈X.∃D∈𝒟. V``{x} ⊆ D"
unfolding UniCovFromUniformity_def by auto
from assms(1) ‹U∈Φ› ‹V∈Φ› have "U∩V ∈ Φ"
unfolding IsUniformity_def IsFilter_def by auto
with assms(1) obtain W where "W∈Φ" and "W O W ⊆ U∩V" and "W=converse(W)"
using half_size_symm by blast
from assms(1) ‹W∈Φ› have "domain(W) ⊆ X"
unfolding IsUniformity_def IsFilter_def by auto
let ?P = "{W``{t}. t∈X}"
have "?P∈Θ" "?P <⇧B 𝒞" "?P <⇧B 𝒟"
proof -
from assms(1,2) ‹W∈Φ› show "?P∈Θ" using cover_image by simp
with assms(2) have "⋃?P = X" unfolding UniCovFromUniformity_def Covers_def
by simp
{ fix x assume "x∈X"
from ‹W=converse(W)› ‹domain(W) ⊆ X› ‹W O W ⊆ U∩V›
have "Star({x},?P) ⊆ U``{x}" and "Star({x},?P) ⊆ V``{x}"
using rel_sq_image by auto
from ‹x∈X› I obtain C where "C∈𝒞" and "U``{x} ⊆ C"
by auto
with ‹Star({x},?P) ⊆ U``{x}› ‹C∈𝒞› have "∃C∈𝒞. Star({x},?P) ⊆ C"
by auto
moreover
from ‹x∈X› II obtain D where "D∈𝒟" and "V``{x} ⊆ D"
by auto
with ‹Star({x},?P) ⊆ V``{x}› ‹D∈𝒟› have "∃D∈𝒟. Star({x},?P) ⊆ D"
by auto
ultimately have "∃C∈𝒞. Star({x},?P) ⊆ C" and "∃D∈𝒟. Star({x},?P) ⊆ D"
by auto
} hence "∀x∈X. ∃C∈𝒞. Star({x},?P) ⊆ C" and "∀x∈X.∃D∈𝒟. Star({x},?P) ⊆ D"
by auto
with ‹⋃?P = X› show "?P <⇧B 𝒞" and "?P <⇧B 𝒟"
unfolding IsBarycentricRefinement_def by auto
qed
thus ?thesis by auto
qed
text‹If $\Phi$ is a (diagonal) uniformity on $X$, then every element
of ‹UniCovFromUniformity(X,Φ)› has a barycentric refinement there.›
corollary bar_refinement_ex:
assumes "Φ {is a uniformity on} X" "Θ = UniCovFromUniformity(X,Φ)" "𝒞 ∈ Θ"
shows "∃ℛ∈Θ. (ℛ <⇧B 𝒞)"
using assms common_bar_refinemnt by blast
text‹ If $\Phi$ is a (diagonal) uniformity on $X$, then ‹UniCovFromUniformity(X,Φ)› is
a family of uniform covers.›
theorem unicov_from_uniformity: assumes "Φ {is a uniformity on} X" and "X≠0"
shows "UniCovFromUniformity(X,Φ) {are uniform covers of} X"
proof -
let ?Θ = "UniCovFromUniformity(X,Φ)"
from assms(1) have "?Θ ⊆ Covers(X)" unfolding UniCovFromUniformity_def
by auto
moreover
from assms(1) have "{X} ∈ ?Θ"
unfolding Covers_def IsUniformity_def IsFilter_def UniCovFromUniformity_def
by auto
hence "?Θ ≠ 0" by auto
moreover have "∀ℛ∈?Θ.∀𝒞∈Covers(X). ((ℛ <⇧* 𝒞) ⟶ 𝒞∈?Θ)"
proof -
{ fix ℛ 𝒞 assume "ℛ∈?Θ" "𝒞∈Covers(X)" "ℛ <⇧* 𝒞"
have "𝒞∈?Θ"
proof -
from ‹ℛ∈?Θ› obtain U where "U∈Φ" and I: "∀x∈X.∃R∈ℛ. U``({x}) ⊆ R"
unfolding UniCovFromUniformity_def by auto
{ fix x assume "x∈X"
with I obtain R where "R∈ℛ" and "U``({x}) ⊆ R" by auto
from ‹R∈ℛ› ‹ℛ <⇧* 𝒞› obtain C where "C∈𝒞" and "Star(R,ℛ) ⊆ C"
unfolding IsStarRefinement_def by auto
with ‹U``({x}) ⊆ R› ‹R∈ℛ› have "U``({x}) ⊆ C"
using element_subset_star by blast
with ‹C∈𝒞› have "∃C∈𝒞. U``({x}) ⊆ C" by auto
} hence "∀x∈X.∃C∈𝒞. U``({x}) ⊆ C" by auto
with ‹U∈Φ› ‹𝒞∈Covers(X)› show ?thesis unfolding UniCovFromUniformity_def
by auto
qed
} thus ?thesis by auto
qed
moreover have "∀𝒞∈?Θ.∀𝒟∈?Θ.∃ℛ∈?Θ.(ℛ <⇧* 𝒞) ∧ (ℛ <⇧* 𝒟)"
proof -
{ fix 𝒞 𝒟 assume "𝒞∈?Θ" "𝒟∈?Θ"
with assms(1) obtain P where "P∈?Θ" and "P <⇧B 𝒞" "P <⇧B 𝒟"
using common_bar_refinemnt by blast
from assms(1) ‹P∈?Θ› obtain ℛ where "ℛ∈?Θ" and "ℛ <⇧B P"
using bar_refinement_ex by blast
from ‹ℛ∈?Θ› ‹P∈?Θ› ‹𝒞∈?Θ› ‹𝒟∈?Θ› have
"P ∈ Covers(X)" "ℛ ∈ Covers(X)" "𝒞 ∈ Covers(X)" "𝒟 ∈ Covers(X)"
unfolding UniCovFromUniformity_def by auto
with assms(2) ‹ℛ <⇧B P› ‹P <⇧B 𝒞› ‹P <⇧B 𝒟› have "ℛ <⇧* 𝒞" and "ℛ <⇧* 𝒟"
using bary_bary_star by auto
with ‹ℛ∈?Θ› have "∃ℛ∈?Θ.(ℛ <⇧* 𝒞) ∧ (ℛ <⇧* 𝒟)" by auto
} thus ?thesis by simp
qed
ultimately show ?thesis unfolding AreUniformCovers_def by simp
qed
text‹ The ‹UniCovFromUniformity› operation is the inverse of ‹UniformityFromUniCov›. ›
theorem unicov_from_unif_inv: assumes "Θ {are uniform covers of} X" "X≠0"
shows "UniCovFromUniformity(X,UniformityFromUniCov(X,Θ)) = Θ"
proof
let ?Φ = "UniformityFromUniCov(X,Θ)"
let ?L = "UniCovFromUniformity(X,?Φ)"
from assms have I: "?Φ {is a uniformity on} X"
using uniformity_from_unicov by simp
with assms(2) have II: "?L {are uniform covers of} X"
using unicov_from_uniformity by simp
{ fix P assume "P∈?L"
with I obtain Q where "Q∈?L" and "Q <⇧B P"
using bar_refinement_ex by blast
from ‹Q∈?L› obtain U where "U∈?Φ" and III:"∀x∈X.∃A∈Q. U``{x} ⊆ A"
unfolding UniCovFromUniformity_def by auto
from ‹U∈?Φ› have "U ∈ Supersets(X×X,{⋃{U×U. U∈P}. P∈Θ})"
unfolding UniformityFromUniCov_def by simp
then obtain B where "B⊆X×X" "B⊆U" and "∃C∈{⋃{U×U. U∈P}. P∈Θ}. C⊆B"
unfolding Supersets_def by auto
then obtain C where "C ∈ {⋃{U×U. U∈P}. P∈Θ}" and "C⊆B" by auto
then obtain R where "R∈Θ" and "C = ⋃{V×V. V∈R}" by auto
with ‹C⊆B› ‹B⊆U› have "⋃{V×V. V∈R} ⊆ U" by auto
from assms(1) II ‹P∈?L› ‹Q∈?L› ‹R∈Θ› have
IV: "P∈Covers(X)" "Q∈Covers(X)" "R∈Covers(X)"
unfolding AreUniformCovers_def by auto
have "R <⇧B Q"
proof -
{ fix x assume "x∈X"
with III obtain A where "A∈Q" and "U``{x} ⊆ A" by auto
with ‹⋃{V×V. V∈R} ⊆ U› have "(⋃{V×V. V∈R})``{x} ⊆ A"
by auto
with ‹A∈Q› have "∃A∈Q. Star({x},R) ⊆ A" using star_singleton by auto
} then have "∀x∈X. ∃A∈Q. Star({x},R) ⊆ A" by simp
moreover from ‹R∈Covers(X)› have "⋃R = X" unfolding Covers_def
by simp
ultimately show ?thesis unfolding IsBarycentricRefinement_def
by simp
qed
with assms(2) ‹Q <⇧B P› IV have "R <⇧* P" using bary_bary_star by simp
with assms(1) ‹R∈Θ› ‹P∈Covers(X)› have "P∈Θ"
unfolding AreUniformCovers_def by simp
} thus "?L⊆Θ" by auto
{ fix P assume "P∈Θ"
with assms(1) have "P ∈ Covers(X)"
unfolding AreUniformCovers_def by auto
from assms(1) ‹P∈Θ› obtain Q where "Q ∈ Θ" and "Q <⇧B P"
using unicov_has_bar_ref by blast
let ?A = "⋃{V×V. V∈Q}"
have "?A ∈ ?Φ"
proof -
from assms(1) ‹Q∈Θ› have "?A ⊆ X×X" and "?A ∈ {⋃{V×V. V∈Q}. Q∈Θ}"
unfolding AreUniformCovers_def Covers_def by auto
then show ?thesis
using superset_gen unfolding UniformityFromUniCov_def
by auto
qed
with I obtain B where "B∈?Φ" "B O B ⊆ ?A" and "B=converse(B)"
using half_size_symm by blast
let ?R = "{B``{x}. x∈X}"
from I II ‹B∈?Φ› have "?R∈?L" and "⋃?R =X"
using cover_image unfolding UniCovFromUniformity_def Covers_def
by auto
have "?R <⇧B P"
proof -
{ fix x assume "x∈X"
from assms(1) ‹Q ∈ Θ› have "⋃Q = X"
unfolding AreUniformCovers_def Covers_def by auto
with ‹Q <⇧B P› ‹x∈X› obtain C where "C∈P" and "Star({x},Q) ⊆ C"
unfolding IsBarycentricRefinement_def by auto
from ‹B=converse(B)› I ‹B∈?Φ› have "Star({x},?R) = (B O B)``{x}"
using uni_domain rel_sq_image by auto
moreover from ‹(B O B) ⊆ ?A› have "(B O B)``{x} ⊆ ?A``{x}" by blast
moreover have "?A``{x} = Star({x},Q)" using star_singleton by simp
ultimately have "Star({x},?R) ⊆ Star({x},Q)" by auto
with ‹Star({x},Q) ⊆ C› ‹C∈P› have "∃C∈P. Star({x},?R) ⊆ C"
by auto
} with ‹⋃?R = X› show ?thesis unfolding IsBarycentricRefinement_def
by auto
qed
with assms(2) II ‹P ∈ Covers(X)› ‹?R∈?L› ‹?R <⇧B P› have "P∈?L"
using unicov_bary_cov by simp
} thus "Θ⊆?L" by auto
qed
text‹The ‹UniformityFromUniCov› operation is the inverse of ‹UniCovFromUniformity›. ›
theorem unif_from_unicov_inv: assumes "Φ {is a uniformity on} X" "X≠0"
shows "UniformityFromUniCov(X,UniCovFromUniformity(X,Φ)) = Φ"
proof
let ?Θ = "UniCovFromUniformity(X,Φ)"
let ?L = "UniformityFromUniCov(X,?Θ)"
from assms have I: "?Θ {are uniform covers of} X"
using unicov_from_uniformity by simp
with assms have II: "?L {is a uniformity on} X"
using uniformity_from_unicov by simp
{ fix A assume "A∈Φ"
with assms(1) obtain B where "B∈Φ" "B O B ⊆ A" and "B = converse(B)"
using half_size_symm by blast
from assms(1) ‹A∈Φ› have "A ⊆ X×X" using uni_domain(1)
by simp
let ?P = "{B``{x}. x∈X}"
from assms(1) ‹B∈Φ› have "?P∈?Θ" using cover_image
by simp
let ?C = "⋃{U×U. U∈?P}"
from I ‹?P∈?Θ› have "?C∈?L"
unfolding AreUniformCovers_def using basic_unif by blast
from assms(1) ‹B∈Φ› ‹B = converse(B)› ‹B O B ⊆ A› have "?C ⊆ A"
using uni_domain(2) symm_sq_prod_image by simp
with II ‹A ⊆ X×X› ‹?C∈?L› have "A∈?L"
unfolding IsUniformity_def IsFilter_def by simp
} thus "Φ⊆?L" by auto
{ fix A assume "A∈?L"
with II have "A ⊆ X×X" using entourage_props(1) by simp
from ‹A∈?L› obtain P where "P∈?Θ" and "⋃{U×U. U∈P} ⊆ A"
unfolding UniformityFromUniCov_def Supersets_def by blast
from ‹P∈?Θ› obtain B where "B∈Φ" and III: "∀x∈X. ∃V∈P. B``{x} ⊆ V"
unfolding UniCovFromUniformity_def by auto
have "B⊆A"
proof -
from assms(1) ‹B∈Φ› have "B ⊆ ⋃{B``{x}×B``{x}. x∈X}"
using entourage_props(1,2) refl_union_singl_image by simp
moreover have "⋃{B``{x}×B``{x}. x∈X} ⊆ A"
proof -
{ fix x assume "x∈X"
with III obtain V where "V∈P" and "B``{x} ⊆ V" by auto
hence "B``{x}×B``{x} ⊆ ⋃{U×U. U∈P}" by auto
} hence "⋃{B``{x}×B``{x}. x∈X} ⊆ ⋃{U×U. U∈P}" by blast
with ‹⋃{U×U. U∈P} ⊆ A› show ?thesis by blast
qed
ultimately show ?thesis by auto
qed
with assms(1) ‹B∈Φ› ‹A ⊆ X×X› have "A∈Φ"
unfolding IsUniformity_def IsFilter_def by simp
} thus "?L⊆Φ" by auto
qed
end