Skip to content

Commit

Permalink
refactor around the definition of base of a uniformity
Browse files Browse the repository at this point in the history
  • Loading branch information
@SKolodynski
SKolodynski committed Jun 29, 2024
1 parent de8c1d8 commit 71e7b9e
Show file tree
Hide file tree
Showing 2 changed files with 74 additions and 43 deletions.
74 changes: 52 additions & 22 deletions IsarMathLib/UniformSpace_ZF.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,18 +56,24 @@ definition
"\<Phi> {is a uniformity on} X \<equiv>(\<Phi> {is a filter on} (X\<times>X))
\<and> (\<forall>U\<in>\<Phi>. id(X) \<subseteq> U \<and> (\<exists>V\<in>\<Phi>. V O V \<subseteq> U) \<and> converse(U) \<in> \<Phi>)"

text\<open>Since the whole $X\times X$ is in a uniformity, a uniformity is never empty.\<close>

lemma uniformity_non_empty: assumes "\<Phi> {is a uniformity on} X"
shows "\<Phi>\<noteq>\<emptyset>"
using assms unfolding IsUniformity_def IsFilter_def by auto

text\<open> 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. \<close>

lemma neigh_not_empty:
assumes "\<Phi> {is a uniformity on} X" "W\<in>\<Phi>" and "x\<in>X"
shows "W``{x} \<noteq> 0" and "x \<in> W``{x}"
shows "W``{x} \<noteq> \<emptyset>" and "x \<in> W``{x}"
proof -
from assms(1,2) have "id(X) \<subseteq> W"
unfolding IsUniformity_def IsFilter_def by auto
with \<open>x\<in>X\<close> show" x\<in>W``{x}" and "W``{x} \<noteq> 0" by auto
with \<open>x\<in>X\<close> show" x\<in>W``{x}" and "W``{x} \<noteq> \<emptyset>" by auto
qed

text\<open>The filter part of the definition of uniformity for easier reference:\<close>
Expand Down Expand Up @@ -181,10 +187,10 @@ proof -
from assms have PhiFilter: "\<Phi> {is a filter on} (X\<times>X)" and
"\<M>:X\<rightarrow>Pow(Pow(X))" and "\<M>`(x) = {V``{x}.V\<in>\<Phi>}"
using IsUniformity_def neigh_filt_fun by auto
have "0 \<notin> \<M>`(x)"
have "\<emptyset> \<notin> \<M>`(x)"
proof -
from assms \<open>x\<in>X\<close> have "0 \<notin> {V``{x}.V\<in>\<Phi>}" using neigh_not_empty by blast
with \<open>\<M>`(x) = {V``{x}.V\<in>\<Phi>}\<close> show "0 \<notin> \<M>`(x)" by simp
from assms \<open>x\<in>X\<close> have "\<emptyset> \<notin> {V``{x}.V\<in>\<Phi>}" using neigh_not_empty by blast
with \<open>\<M>`(x) = {V``{x}.V\<in>\<Phi>}\<close> show "\<emptyset> \<notin> \<M>`(x)" by simp
qed
moreover have "X \<in> \<M>`(x)"
proof -
Expand Down Expand Up @@ -452,7 +458,7 @@ proof
moreover from \<open>z = \<langle>?x,?y\<rangle>\<close> have "{?x}\<times>{?y} = {z}"
by (rule pair_prod)
ultimately have "(W``{?x})\<times>(W``{?y}) \<in> ?M`{z}" by simp
with zMem JJtop \<open>R \<subseteq> \<Union>(J\<times>\<^sub>tJ)\<close> have "(W``{?x})\<times>(W``{?y}) \<inter> R \<noteq> 0"
with zMem JJtop \<open>R \<subseteq> \<Union>(J\<times>\<^sub>tJ)\<close> have "(W``{?x})\<times>(W``{?y}) \<inter> R \<noteq> \<emptyset>"
using neindisj by blast
with assms(4) have "\<langle>?x,?y\<rangle> \<in> W O (R O W)"
using sym_rel_comp by simp
Expand Down Expand Up @@ -578,13 +584,17 @@ text\<open>Analogous to the predicate "satisfies base condition" (defined in \<o
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$.\<close>
such that $B_2\circ B_2 \subseteq B_1$.
The conditions are taken from
N. Bourbaki "Elements of Mathematics, General Topology", Chapter II.1.,
except for the last two that are missing there.\<close>

definition
IsUniformityBaseOn ("_ {is a uniform base on} _" 90) where
"\<BB> {is a uniform base on} X \<equiv>
(\<forall>B\<^sub>1\<in>\<BB>. \<forall>B\<^sub>2\<in>\<BB>. \<exists>B\<^sub>3\<in>\<BB>. B\<^sub>3\<subseteq>B\<^sub>1\<inter>B\<^sub>2) \<and> (\<forall>B\<in>\<BB>. id(X)\<subseteq>B) \<and>
(\<forall>B\<^sub>1\<in>\<BB>. \<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 \<subseteq> converse(B\<^sub>1)) \<and> (\<forall>B\<^sub>1\<in>\<BB>. \<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 O B\<^sub>2 \<subseteq> B\<^sub>1)"
(\<forall>B\<^sub>1\<in>\<BB>. \<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 \<subseteq> converse(B\<^sub>1)) \<and> (\<forall>B\<^sub>1\<in>\<BB>. \<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 O B\<^sub>2 \<subseteq> B\<^sub>1) \<and>
\<BB>\<subseteq>Pow(X\<times>X) \<and> \<BB>\<noteq>\<emptyset>"

text\<open>The next lemma splits the definition of \<open>IsUniformityBaseOn\<close> into four conditions
to enable more precise references in proofs.\<close>
Expand All @@ -595,6 +605,7 @@ lemma uniformity_base_props: assumes "\<BB> {is a uniform base on} X"
"\<forall>B\<in>\<BB>. id(X)\<subseteq>B"
"\<forall>B\<^sub>1\<in>\<BB>. \<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 \<subseteq> converse(B\<^sub>1)"
"\<forall>B\<^sub>1\<in>\<BB>. \<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 O B\<^sub>2 \<subseteq> B\<^sub>1"
"\<BB>\<subseteq>Pow(X\<times>X)" and "\<BB>\<noteq>\<emptyset>"
using assms unfolding IsUniformityBaseOn_def by simp_all

text\<open>If supersets of some collection of subsets of $X\times X$ form a uniformity,
Expand Down Expand Up @@ -640,36 +651,41 @@ proof -
with \<open>B\<^sub>2\<in>\<BB>\<close> have "\<exists>B\<^sub>2\<in>\<BB>. B\<^sub>2 O B\<^sub>2 \<subseteq> B\<^sub>1" by auto
} thus ?thesis by simp
qed
moreover from assms(2) have "\<BB>\<noteq>\<emptyset>"
using supersets_of_empty uniformity_non_empty by blast
ultimately show "\<BB> {is a uniform base on} X"
unfolding IsUniformityBaseOn_def by simp
unfolding IsUniformityBaseOn_def using assms(1) by simp
qed

text\<open>if a nonempty collection of subsets of $X\times X$ satisfies conditions in the definition
of \<open>IsUniformityBaseOn\<close> then the supersets of that collection form a uniformity on $X$. \<close>
of \<open>IsUniformityBaseOn\<close> then the supersets of that collection form a uniformity on $X$.\<close>

theorem uniformity_base_is_base:
assumes "\<BB>\<noteq>0" "X\<noteq>0" "\<BB>\<subseteq>Pow(X\<times>X)" and "\<BB> {is a uniform base on} X"
shows "(Supersets(X\<times>X,\<BB>) {is a uniformity on} X)"
assumes "X\<noteq>\<emptyset>" and "\<BB> {is a uniform base on} X"
shows "Supersets(X\<times>X,\<BB>) {is a uniformity on} X"
proof -
let ?\<Phi> = "Supersets(X\<times>X,\<BB>)"
from assms(2) have "\<BB>\<subseteq>Pow(X\<times>X)" using uniformity_base_props(5)
by simp
have "?\<Phi> {is a filter on} (X\<times>X)"
proof -
from assms have "0\<notin>?\<Phi>"
from assms have "\<emptyset>\<notin>?\<Phi>"
unfolding Supersets_def using uniformity_base_props(2)
by blast
moreover have "X\<times>X \<in> ?\<Phi>"
proof -
from assms(1) obtain B where "B\<in>\<BB>" by auto
with assms(3) have "B\<subseteq>X\<times>X" by auto
with \<open>B\<in>\<BB>\<close> show "X\<times>X \<in> ?\<Phi>" unfolding Supersets_def by auto
from assms(2) obtain B where "B\<in>\<BB>"
using uniformity_base_props(6) by blast
with \<open>\<BB>\<subseteq>Pow(X\<times>X)\<close> show "X\<times>X \<in> ?\<Phi>" unfolding Supersets_def
by blast
qed
moreover have "?\<Phi> \<subseteq> Pow(X\<times>X)" unfolding Supersets_def by auto
moreover have "\<forall>U\<in>?\<Phi>. \<forall>V\<in>?\<Phi>. U\<inter>V \<in> ?\<Phi>"
proof -
{ fix U V assume "U\<in>?\<Phi>" "V\<in>?\<Phi>"
then obtain B\<^sub>1 B\<^sub>2 where "B\<^sub>1\<in>\<BB>" "B\<^sub>2\<in>\<BB>" "B\<^sub>1\<subseteq>U" "B\<^sub>2\<subseteq>V"
unfolding Supersets_def by auto
from assms(4) \<open>B\<^sub>1\<in>\<BB>\<close> \<open>B\<^sub>2\<in>\<BB>\<close> obtain B\<^sub>3 where "B\<^sub>3\<in>\<BB>" and "B\<^sub>3\<subseteq>B\<^sub>1\<inter>B\<^sub>2"
from assms(2) \<open>B\<^sub>1\<in>\<BB>\<close> \<open>B\<^sub>2\<in>\<BB>\<close> obtain B\<^sub>3 where "B\<^sub>3\<in>\<BB>" and "B\<^sub>3\<subseteq>B\<^sub>1\<inter>B\<^sub>2"
using uniformity_base_props(1) by blast
from \<open>B\<^sub>1\<subseteq>U\<close> \<open>B\<^sub>2\<subseteq>V\<close> \<open>B\<^sub>3\<subseteq>B\<^sub>1\<inter>B\<^sub>2\<close> have "B\<^sub>3\<subseteq>U\<inter>V" by auto
with \<open>U\<in>?\<Phi>\<close> \<open>V\<in>?\<Phi>\<close> \<open>B\<^sub>3\<in>\<BB>\<close> have "U\<inter>V \<in> ?\<Phi>"
Expand All @@ -693,15 +709,15 @@ proof -
{ fix U assume "U\<in>?\<Phi>"
then obtain B where "B\<in>\<BB>" and "B\<subseteq>U"
unfolding Supersets_def by auto
with assms(4) have "id(X) \<subseteq> U"
with assms(2) have "id(X) \<subseteq> U"
using uniformity_base_props(2) by blast
moreover
from assms(4) \<open>B\<in>\<BB>\<close> obtain V where "V\<in>\<BB>" and "V O V \<subseteq> B"
from assms(2) \<open>B\<in>\<BB>\<close> obtain V where "V\<in>\<BB>" and "V O V \<subseteq> B"
using uniformity_base_props(4) by blast
with assms(3) have "V\<in>?\<Phi>" using superset_gen by auto
with \<open>\<BB>\<subseteq>Pow(X\<times>X)\<close> have "V\<in>?\<Phi>" using superset_gen by auto
with \<open>V O V \<subseteq> B\<close> \<open>B\<subseteq>U\<close> have "\<exists>V\<in>?\<Phi>. V O V \<subseteq> U" by blast
moreover
from assms(4) \<open>B\<in>\<BB>\<close> \<open>B\<subseteq>U\<close> obtain W where "W\<in>\<BB>" and "W \<subseteq> converse(U)"
from assms(2) \<open>B\<in>\<BB>\<close> \<open>B\<subseteq>U\<close> obtain W where "W\<in>\<BB>" and "W \<subseteq> converse(U)"
using uniformity_base_props(3) by blast
with \<open>U\<in>?\<Phi>\<close> have "converse(U) \<in> ?\<Phi>" unfolding Supersets_def
by auto
Expand All @@ -711,5 +727,19 @@ proof -
qed
ultimately show ?thesis unfolding IsUniformity_def by simp
qed


text\<open>The assumption that $X$ is empty in \<open>uniformity_base_is_base\<close> above is neccessary
as the assertion is false if $X$ is empty.\<close>

lemma uniform_space_empty: assumes "\<BB> {is a uniform base on} \<emptyset>"
shows "\<not>(Supersets(\<emptyset>\<times>\<emptyset>,\<BB>) {is a uniformity on} \<emptyset>)"
proof -
{ let ?\<Phi> = "Supersets(\<emptyset>\<times>\<emptyset>,\<BB>)"
assume "?\<Phi> {is a uniformity on} \<emptyset>"
from assms have "\<BB>={\<emptyset>}" using uniformity_base_props(5,6) by force
with \<open>?\<Phi> {is a uniformity on} \<emptyset>\<close> have False
using supersets_in_empty unif_filter unfolding IsFilter_def by auto
} thus ?thesis by auto
qed

end
43 changes: 22 additions & 21 deletions IsarMathLib/ZF1.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,16 +55,22 @@ proof
with assms show "x \<in> \<Union>B" by auto
qed

text\<open>In ZF set theory the zero of natural numbers is the same as the empty set.
In the next abbreviation we declare that we want $0$ and $\emptyset$ to be synonyms
so that we can use $\emptyset$ instead of $0$ when appropriate. \<close>

abbreviation empty_set ("\<emptyset>") where "\<emptyset> \<equiv> 0"

text\<open>If all sets of a nonempty collection are the same, then its union
is the same.\<close>

lemma ZF1_1_L1: assumes "C\<noteq>0" and "\<forall>y\<in>C. b(y) = A"
lemma ZF1_1_L1: assumes "C\<noteq>\<emptyset>" and "\<forall>y\<in>C. b(y) = A"
shows "(\<Union>y\<in>C. b(y)) = A" using assms by blast

text\<open>The union af all values of a constant meta-function belongs to
the same set as the constant.\<close>

lemma ZF1_1_L2: assumes A1:"C\<noteq>0" and A2: "\<forall>x\<in>C. b(x) \<in> A"
lemma ZF1_1_L2: assumes A1:"C\<noteq>\<emptyset>" and A2: "\<forall>x\<in>C. b(x) \<in> A"
and A3: "\<forall>x y. x\<in>C \<and> y\<in>C \<longrightarrow> b(x) = b(y)"
shows "(\<Union>x\<in>C. b(x))\<in>A"
proof -
Expand Down Expand Up @@ -120,7 +126,7 @@ qed
text\<open>A lemma about inclusion in cartesian products. Included here to remember
that we need the $U\times V \neq \emptyset$ assumption.\<close>

lemma prod_subset: assumes "U\<times>V\<noteq>0" "U\<times>V \<subseteq> X\<times>Y" shows "U\<subseteq>X" and "V\<subseteq>Y"
lemma prod_subset: assumes "U\<times>V\<noteq>\<emptyset>" "U\<times>V \<subseteq> X\<times>Y" shows "U\<subseteq>X" and "V\<subseteq>Y"
using assms by auto

text\<open>A technical lemma about sections in cartesian products.\<close>
Expand All @@ -138,7 +144,7 @@ lemma ZF1_1_L4B: assumes "\<forall>x\<in>X. a(x) = b(x)"

text\<open>A set defined by a constant meta-function is a singleton.\<close>

lemma ZF1_1_L5: assumes "X\<noteq>0" and "\<forall>x\<in>X. b(x) = c"
lemma ZF1_1_L5: assumes "X\<noteq>\<emptyset>" and "\<forall>x\<in>X. b(x) = c"
shows "{b(x). x\<in>X} = {c}" using assms by blast

text\<open>Most of the time, \<open>auto\<close> does this job, but there are strange
Expand All @@ -150,13 +156,13 @@ lemma subset_with_property: assumes "Y = {x\<in>X. b(x)}"

text\<open>We can choose an element from a nonempty set.\<close>

lemma nonempty_has_element: assumes "X\<noteq>0" shows "\<exists>x. x\<in>X"
lemma nonempty_has_element: assumes "X\<noteq>\<emptyset>" shows "\<exists>x. x\<in>X"
using assms by auto

(*text{*If after removing an element from a set we get an empty set,
then this set must be a singleton.*}
lemma rem_point_empty: assumes "a\<in>A" and "A-{a} = 0"
lemma rem_point_empty: assumes "a\<in>A" and "A-{a} = \<emptyset>"
shows "A = {a}" using assms by auto; *)

text\<open>In Isabelle/ZF the intersection of an empty family is
Expand All @@ -165,13 +171,13 @@ text\<open>In Isabelle/ZF the intersection of an empty family is
difficult to find. This is one reason we need comments before every
theorem: so that we can search for keywords.\<close>

lemma inter_empty_empty: shows "\<Inter>0 = 0" by (rule Inter_0)
lemma inter_empty_empty: shows "\<Inter>\<emptyset> = \<emptyset>" by (rule Inter_0)

text\<open>If an intersection of a collection is not empty, then the collection is
not empty. We are (ab)using the fact the the intersection of empty collection
is defined to be empty.\<close>

lemma inter_nempty_nempty: assumes "\<Inter>A \<noteq> 0" shows "A\<noteq>0"
lemma inter_nempty_nempty: assumes "\<Inter>A \<noteq> \<emptyset>" shows "A\<noteq>\<emptyset>"
using assms by auto

text\<open>For two collections $S,T$ of sets we define the product collection
Expand All @@ -188,7 +194,7 @@ lemma ZF1_1_L6: shows "\<Union> ProductCollection(S,T) = \<Union>S \<times> \<Un

text\<open>An intersection of subsets is a subset.\<close>

lemma ZF1_1_L7: assumes A1: "I\<noteq>0" and A2: "\<forall>i\<in>I. P(i) \<subseteq> X"
lemma ZF1_1_L7: assumes A1: "I\<noteq>\<emptyset>" and A2: "\<forall>i\<in>I. P(i) \<subseteq> X"
shows "( \<Inter>i\<in>I. P(i) ) \<subseteq> X"
proof -
from A1 obtain i\<^sub>0 where "i\<^sub>0 \<in> I" by auto
Expand Down Expand Up @@ -306,8 +312,8 @@ lemma consdef: shows "cons(a,A) = A \<union> {a}"
text\<open>If a difference between a set and a singleton is empty, then
the set is empty or it is equal to the singleton.\<close>

lemma singl_diff_empty: assumes "A - {x} = 0"
shows "A = 0 \<or> A = {x}"
lemma singl_diff_empty: assumes "A - {x} = \<emptyset>"
shows "A = \<emptyset> \<or> A = {x}"
using assms by auto

text\<open>If a difference between a set and a singleton is the set,
Expand Down Expand Up @@ -419,7 +425,7 @@ text\<open>If the cartesian product of the images of $x$ and $y$ by a
then $x$ is in relation $W\circ (R\circ W)$ with $y$. \<close>

lemma sym_rel_comp:
assumes "W=converse(W)" and "(W``{x})\<times>(W``{y}) \<inter> R \<noteq> 0"
assumes "W=converse(W)" and "(W``{x})\<times>(W``{y}) \<inter> R \<noteq> \<emptyset>"
shows "\<langle>x,y\<rangle> \<in> (W O (R O W))"
proof -
from assms(2) obtain s t where "s\<in>W``{x}" "t\<in>W``{y}" and "\<langle>s,t\<rangle>\<in>R"
Expand Down Expand Up @@ -447,7 +453,7 @@ lemma superset_gen: assumes "A\<subseteq>X" "A\<in>\<A>" shows "A \<in> Superset

text\<open>The whole space is a superset of any nonempty collection of its subsets. \<close>

lemma space_superset: assumes "\<A>\<noteq>0" "\<A>\<subseteq>Pow(X)" shows "X \<in> Supersets(X,\<A>)"
lemma space_superset: assumes "\<A>\<noteq>\<emptyset>" "\<A>\<subseteq>Pow(X)" shows "X \<in> Supersets(X,\<A>)"
proof -
from assms(1) obtain A where "A\<in>\<A>" by auto
with assms(2) show ?thesis unfolding Supersets_def by auto
Expand All @@ -456,14 +462,14 @@ qed
text\<open>The collection of supersets of an empty set is empty. In particular
the whole space $X$ is not a superset of an empty set. \<close>

lemma supersets_of_empty: shows "Supersets(X,0) = 0"
lemma supersets_of_empty: shows "Supersets(X,\<emptyset>) = \<emptyset>"
unfolding Supersets_def by auto

text\<open>However, when the space is empty the collection of supersets does not have
to be empty - the collection of supersets of the singleton collection containing
only the empty set is this collection. \<close>

lemma supersets_in_empty: shows "Supersets(0,{0}) = {0}"
lemma supersets_in_empty: shows "Supersets(\<emptyset>,{\<emptyset>}) = {\<emptyset>}"
unfolding Supersets_def by auto

text\<open>This can be done by the auto method, but sometimes takes a long time. \<close>
Expand Down Expand Up @@ -499,7 +505,7 @@ lemma set_comp_eq: assumes "\<forall>x\<in>X. p(x) = q(x)"
text\<open>If every element of a non-empty set $X\subseteq Y$ satisfies a condition
then the set of elements of $Y$ that satisfy the condition is non-empty.\<close>

lemma non_empty_cond: assumes "X\<noteq>0" "X\<subseteq>Y" and "\<forall>x\<in>X. P(x)"
lemma non_empty_cond: assumes "X\<noteq>\<emptyset>" "X\<subseteq>Y" and "\<forall>x\<in>X. P(x)"
shows "{x\<in>Y. P(x)} \<noteq> 0" using assms by auto

text\<open>If $z$ is a pair, then the cartesian product of the singletons of its
Expand All @@ -515,11 +521,6 @@ text\<open>In Isabelle/ZF the set difference is written with a minus sign $A-B$

abbreviation set_difference (infixl "\<setminus>" 65) where "A\<setminus>B \<equiv> A-B"

text\<open>In ZF set theory the zero of natural numbers is the same as the empty set.
In the next abbreviation we declare that we want $0$ and $\emptyset$ to be synonyms
so that we can use $\emptyset$ instead of $0$ when appropriate. \<close>

abbreviation empty_set ("\<emptyset>") where "\<emptyset> \<equiv> 0"

end

0 comments on commit 71e7b9e

Please sign in to comment.