(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2021-2022 Slawomir Kolodynski This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) 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 an alternative definition based of the notion of uniform covers. › 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