Theory KuratowskiClosureComplementTheorem
theory KuratowskiClosureComplementTheorem
imports
"HOL-Analysis.Multivariate_Analysis"
"HOL-Analysis.Continuum_Not_Denumerable"
begin
section‹ Introduction ›
text‹
We discuss a topological curiosity discovered by \<^cite>‹"Kuratowski:1922"›: the fact that the number of distinct operators on
a topological space generated by compositions of closure and
complement never exceeds 14, and is exactly 14 in the case of @{term
"ℝ"}. In addition, we prove a theorem due to \<^cite>‹"Chagrov:1982"› that classifies topological spaces according to the
number of such operators they support.
Kuratowski's result, which is exposited in \<^cite>‹"TheoremOfTheDay:2015"› and Chapter 7 of \<^cite>‹"Chamberland:2015"›,
has already been treated in Mizar --- see \<^cite>‹"BaginskaGrabowski:2003"› and \<^cite>‹"Grabowski:2004"›. To the best of
our knowledge, we are the first to mechanize Chagrov's result.
Our work is based on a presentation of Kuratowski's and Chagrov's
results by \<^cite>‹"GardnerJackson:2008"›.
We begin with some preliminary facts pertaining to the relationship
between interiors of unions and unions of interiors
(\S\ref{sec:interiors-unions}) and the relationship between @{term
"ℚ"} and @{term "ℝ"} (\S\ref{sec:rat-real}). We then prove
Kuratowski's result (\S\ref{sec:kuratowski}) and the corollary that at
most 7 distinct operators on a topological space can be generated by
compositions of closure and interior
(\S\ref{sec:kuratowski-corollary}). Finally, we prove Chagrov's result
(\S\ref{sec:chagrov}).
›
section‹ Interiors and unions \label{sec:interiors-unions} ›
definition
boundary :: "'a::topological_space set ⇒ 'a set"
where
"boundary X = closure X - interior X"
lemma boundary_empty:
shows "boundary {} = {}"
unfolding boundary_def by simp
definition
exterior :: "'a::topological_space set ⇒ 'a set"
where
"exterior X = - (interior X ∪ boundary X)"
lemma interior_union_boundary:
shows "interior (X ∪ Y) = interior X ∪ interior Y
⟷ boundary X ∩ boundary Y ⊆ boundary (X ∪ Y)" (is "(?lhs1 = ?lhs2) ⟷ ?rhs")
proof(rule iffI[OF _ subset_antisym[OF subsetI]])
assume "?lhs1 = ?lhs2" then show ?rhs by (force simp: boundary_def)
next
fix x
assume ?rhs and "x ∈ ?lhs1"
have "x ∈ ?lhs2" if "x ∉ interior X" "x ∉ interior Y"
proof(cases "x ∈ boundary X ∩ boundary Y")
case True with ‹?rhs› ‹x ∈ ?lhs1› show ?thesis by (simp add: boundary_def subset_iff)
next
case False then consider (X) "x ∉ boundary X" | (Y) "x ∉ boundary Y" by blast
then show ?thesis
proof cases
case X
from X ‹x ∉ interior X› have "x ∈ exterior X" by (simp add: exterior_def)
from ‹x ∉ boundary X› ‹x ∈ exterior X› ‹x ∉ interior X›
obtain U where "open U" "U ⊆ - X" "x ∈ U"
by (metis ComplI DiffI boundary_def closure_interior interior_subset open_interior)
from ‹x ∈ interior (X ∪ Y)› obtain U' where "open U'" "U' ⊆ X ∪ Y" "x ∈ U'"
by (meson interiorE)
from ‹U ⊆ - X› ‹U' ⊆ X ∪ Y› have "U ∩ U' ⊆ Y" by blast
with ‹x ∉ interior Y› ‹open U'› ‹open U› ‹x ∈ U'› ‹x ∈ U› show ?thesis
by (meson IntI interiorI open_Int)
next
case Y
from Y ‹x ∉ interior Y› have "x ∈ exterior Y" by (simp add: exterior_def)
from ‹x ∉ boundary Y› ‹x ∈ exterior Y› ‹x ∉ interior Y›
obtain U where "open U" "U ⊆ - Y" "x ∈ U"
by (metis ComplI DiffI boundary_def closure_interior interior_subset open_interior)
from ‹x ∈ interior (X ∪ Y)› obtain U' where "open U'" "U' ⊆ X ∪ Y" "x ∈ U'"
by (meson interiorE)
from ‹U ⊆ -Y› ‹U' ⊆ X ∪ Y› have "U ∩ U' ⊆ X" by blast
with ‹x ∉ interior X› ‹open U'› ‹open U› ‹x ∈ U'› ‹x ∈ U› show ?thesis
by (meson IntI interiorI open_Int)
qed
qed
with ‹x ∈ ?lhs1› show "x ∈ ?lhs2" by blast
next
show "?lhs2 ⊆ ?lhs1" by (simp add: interior_mono)
qed
lemma interior_union_closed_intervals:
fixes a :: "'a::ordered_euclidean_space"
assumes "b < c"
shows "interior ({a..b} ∪ {c..d}) = interior {a..b} ∪ interior {c..d}"
using assms by (subst interior_union_boundary; auto simp: boundary_def)
section‹ Additional facts about the rationals and reals \label{sec:rat-real} ›
lemma Rat_real_limpt:
fixes x :: real
shows "x islimpt ℚ"
proof(rule islimptI)
fix T assume "x ∈ T" "open T"
then obtain e where "0 < e" and ball: "¦x' - x¦ < e ⟶ x' ∈ T" for x' by (auto simp: open_real)
from ‹0 < e› obtain q where "x < real_of_rat q ∧ real_of_rat q < x + e" using of_rat_dense by force
with ball show "∃y∈ℚ. y ∈ T ∧ y ≠ x" by force
qed
lemma Rat_closure:
shows "closure ℚ = (UNIV :: real set)"
unfolding closure_def using Rat_real_limpt by blast
lemma Rat_interval_closure:
fixes x :: real
assumes "x < y"
shows "closure ({x<..<y} ∩ ℚ) = {x..y}"
using assms
by (metis (no_types, lifting) Rat_closure closure_closure closure_greaterThanLessThan closure_mono inf_le1 inf_top.right_neutral open_Int_closure_subset open_real_greaterThanLessThan subset_antisym)
lemma Rat_not_open:
fixes T :: "real set"
assumes "open T"
assumes "T ≠ {}"
shows "¬T ⊆ ℚ"
using assms by (simp add: countable_rat open_minus_countable subset_eq)
lemma Irrat_dense_in_real:
fixes x :: real
assumes "x < y"
shows "∃r∈-ℚ. x < r ∧ r < y"
using assms Rat_not_open[where T="{x<..<y}"] by force
lemma closed_interval_Int_compl:
fixes x :: real
assumes "x < y"
assumes "y < z"
shows "- {x..y} ∩ - {y..z} = - {x..z}"
using assms by auto
section‹ Kuratowski's result \label{sec:kuratowski} ›
text‹
We prove that at most 14 distinct operators can be generated by compositions of @{const "closure"} and complement. For convenience, we give these operators short names and try to avoid pointwise reasoning. We treat the @{const "interior"} operator at the same time.
›
declare o_apply[simp del]
definition C :: "'a::topological_space set ⇒ 'a set" where "C X = - X"
definition K :: "'a::topological_space set ⇒ 'a set" where "K X = closure X"
definition I :: "'a::topological_space set ⇒ 'a set" where "I X = interior X"
lemma C_C:
shows "C ∘ C = id"
by (simp add: fun_eq_iff C_def o_apply)
lemma K_K:
shows "K ∘ K = K"
by (simp add: fun_eq_iff K_def o_apply)
lemma I_I:
shows "I ∘ I = I"
unfolding I_def by (simp add: o_def)
lemma I_K:
shows "I = C ∘ K ∘ C"
unfolding C_def I_def K_def by (simp add: o_def interior_closure)
lemma K_I:
shows "K = C ∘ I ∘ C"
unfolding C_def I_def K_def by (simp add: o_def interior_closure)
lemma K_I_K_I:
shows "K ∘ I ∘ K ∘ I = K ∘ I"
unfolding C_def I_def K_def
by (clarsimp simp: fun_eq_iff o_apply closure_minimal closure_mono closure_subset interior_maximal interior_subset subset_antisym)
lemma I_K_I_K:
shows "I ∘ K ∘ I ∘ K = I ∘ K"
unfolding C_def I_def K_def
by (simp add: fun_eq_iff o_apply)
(metis (no_types) closure_closure closure_mono closure_subset interior_maximal interior_mono interior_subset open_interior subset_antisym)
lemma K_mono:
assumes "x ⊆ y"
shows "K x ⊆ K y"
using assms unfolding K_def by (simp add: closure_mono)
text‹
The following lemma embodies the crucial observation about compositions of @{const "C"} and @{const "K"}:
›
lemma KCKCKCK_KCK:
shows "K ∘ C ∘ K ∘ C ∘ K ∘ C ∘ K = K ∘ C ∘ K" (is "?lhs = ?rhs")
proof(rule ext[OF equalityI])
fix x
have "(C ∘ K ∘ C ∘ K ∘ C ∘ K) x ⊆ ?rhs x" by (simp add: C_def K_def closure_def o_apply)
then have "(K ∘ (C ∘ K ∘ C ∘ K ∘ C ∘ K)) x ⊆ (K ∘ ?rhs) x" by (simp add: K_mono o_apply)
then show "?lhs x ⊆ ?rhs x" by (simp add: K_K o_assoc)
next
fix x :: "'a::topological_space set"
have "(C ∘ K ∘ C ∘ K) x ⊆ K x" by (simp add: C_def K_def closure_def o_apply)
then have "(K ∘ (C ∘ K ∘ C ∘ K)) x ⊆ (K ∘ K) x" by (simp add: K_mono o_apply)
then have "(C ∘ (K ∘ K)) x ⊆ (C ∘ (K ∘ (C ∘ K ∘ C ∘ K))) x" by (simp add: C_def o_apply)
then have "(K ∘ (C ∘ (K ∘ K))) x ⊆ (K ∘ (C ∘ (K ∘ (C ∘ K ∘ C ∘ K)))) x" by (simp add: K_mono o_apply)
then show "?rhs x ⊆ ?lhs x" by (simp add: K_K o_assoc)
qed
text‹
The inductive set ‹CK› captures all operators that can be generated by compositions of @{const "C"} and @{const "K"}. We shallowly embed the operators; that is, we identify operators up to extensional equality.
›
inductive CK :: "('a::topological_space set ⇒ 'a set) ⇒ bool" where
"CK C"
| "CK K"
| "⟦ CK f; CK g ⟧ ⟹ CK (f ∘ g)"
declare CK.intros[intro!]
lemma CK_id[intro!]:
"CK id"
by (metis CK.intros(1) CK.intros(3) C_C)
text‹
The inductive set ‹CK_nf› captures the normal forms for the 14 distinct operators.
›
inductive CK_nf :: "('a::topological_space set ⇒ 'a set) ⇒ bool" where
"CK_nf id"
| "CK_nf C"
| "CK_nf K"
| "CK_nf (C ∘ K)"
| "CK_nf (K ∘ C)"
| "CK_nf (C ∘ K ∘ C)"
| "CK_nf (K ∘ C ∘ K)"
| "CK_nf (C ∘ K ∘ C ∘ K)"
| "CK_nf (K ∘ C ∘ K ∘ C)"
| "CK_nf (C ∘ K ∘ C ∘ K ∘ C)"
| "CK_nf (K ∘ C ∘ K ∘ C ∘ K)"
| "CK_nf (C ∘ K ∘ C ∘ K ∘ C ∘ K)"
| "CK_nf (K ∘ C ∘ K ∘ C ∘ K ∘ C)"
| "CK_nf (C ∘ K ∘ C ∘ K ∘ C ∘ K ∘ C)"
declare CK_nf.intros[intro!]
lemma CK_nf_set:
shows "{f . CK_nf f} = {id, C, K, C ∘ K, K ∘ C, C ∘ K ∘ C, K ∘ C ∘ K, C ∘ K ∘ C ∘ K, K ∘ C ∘ K ∘ C, C ∘ K ∘ C ∘ K ∘ C, K ∘ C ∘ K ∘ C ∘ K, C ∘ K ∘ C ∘ K ∘ C ∘ K, K ∘ C ∘ K ∘ C ∘ K ∘ C, C ∘ K ∘ C ∘ K ∘ C ∘ K ∘ C}"
by (auto simp: CK_nf.simps)
text‹
That each operator generated by compositions of @{const "C"} and
@{const "K"} is extensionally equivalent to one of the normal forms
captured by ‹CK_nf› is demonstrated by means of an
induction over the construction of ‹CK_nf› and an appeal
to the facts proved above.
›
theorem CK_nf:
"CK f ⟷ CK_nf f"
proof(rule iffI)
assume "CK f" then show "CK_nf f"
by induct
(elim CK_nf.cases; clarsimp simp: id_def[symmetric] C_C K_K KCKCKCK_KCK o_assoc; simp add: o_assoc[symmetric]; clarsimp simp: C_C K_K KCKCKCK_KCK o_assoc
| blast)+
next
assume "CK_nf f" then show "CK f" by induct (auto simp: id_def[symmetric])
qed
theorem CK_card:
shows "card {f. CK f} ≤ 14"
by (auto simp: CK_nf CK_nf_set card.insert_remove intro!: le_trans[OF card_Diff1_le])
text‹
We show, using the following subset of ‹ℝ› (an
example taken from \<^cite>‹"Rusin:2001"›) as a witness, that there
exist topological spaces on which all 14 operators are distinct.
›
definition
RRR :: "real set"
where
"RRR = {0<..<1} ∪ {1<..<2} ∪ {3} ∪ ({5<..<7} ∩ ℚ)"
text‹
The following facts allow the required proofs to proceed by @{method simp}:
›
lemma RRR_closure:
shows "closure RRR = {0..2} ∪ {3} ∪ {5..7}"
unfolding RRR_def by (force simp: closure_insert Rat_interval_closure)
lemma RRR_interior:
"interior RRR = {0<..<1} ∪ {1<..<2}" (is "?lhs = ?rhs")
proof(rule equalityI[OF subsetI subsetI])
fix x assume "x ∈ ?lhs"
then obtain T where "open T" and "x ∈ T" and "T ⊆ RRR" by (blast elim: interiorE)
then obtain e where "0 < e" and "ball x e ⊆ T" by (blast elim!: openE)
from ‹x ∈ T› ‹0 < e› ‹ball x e ⊆ T› ‹T ⊆ RRR›
have False if "x = 3"
using that unfolding RRR_def ball_def
by (auto dest!: subsetD[where c="min (3 + e/2) 4"] simp: dist_real_def)
moreover
from Irrat_dense_in_real[where x="x" and y="x + e/2"] ‹0 < e›
obtain r where "r∈- ℚ ∧ x < r ∧ r < x + e / 2" by auto
with ‹x ∈ T› ‹ball x e ⊆ T› ‹T ⊆ RRR›
have False if "x ∈ {5<..<7} ∩ ℚ"
using that unfolding RRR_def ball_def
by (force simp: dist_real_def dest: subsetD[where c=r])
moreover note ‹x ∈ interior RRR›
ultimately show "x ∈ ?rhs"
unfolding RRR_def by (auto dest: subsetD[OF interior_subset])
next
fix x assume "x ∈ ?rhs"
then show "x ∈ ?lhs"
unfolding RRR_def interior_def by (auto intro: open_real_greaterThanLessThan)
qed
lemma RRR_interior_closure[simplified]:
shows "interior ({0::real..2} ∪ {3} ∪ {5..7}) = {0<..<2} ∪ {5<..<7}" (is "?lhs = ?rhs")
proof -
have "?lhs = interior ({0..2} ∪ {5..7})"
by (metis (no_types, lifting) Un_assoc Un_commute closed_Un closed_eucl_atLeastAtMost interior_closed_Un_empty_interior interior_singleton)
also have "... = ?rhs"
by (simp add: interior_union_closed_intervals)
finally show ?thesis .
qed
text‹
The operators can be distinguished by testing which of the points in
‹{1,2,3,4,6}› belong to their results.
›
definition
test :: "(real set ⇒ real set) ⇒ bool list"
where
"test f ≡ map (λx. x ∈ f RRR) [1,2,3,4,6]"
lemma RRR_test:
assumes "f RRR = g RRR"
shows "test f = test g"
unfolding test_def using assms by simp
lemma nf_RRR:
shows
"test id = [False, False, True, False, True]"
"test C = [True, True, False, True, False]"
"test K = [True, True, True, False, True]"
"test (K ∘ C) = [True, True, True, True, True]"
"test (C ∘ K) = [False, False, False, True, False]"
"test (C ∘ K ∘ C) = [False, False, False, False, False]"
"test (K ∘ C ∘ K) = [False, True, True, True, False]"
"test (C ∘ K ∘ C ∘ K) = [True, False, False, False, True]"
"test (K ∘ C ∘ K ∘ C) = [True, True, False, False, False]"
"test (C ∘ K ∘ C ∘ K ∘ C) = [False, False, True, True, True]"
"test (K ∘ C ∘ K ∘ C ∘ K) = [True, True, False, False, True]"
"test (C ∘ K ∘ C ∘ K ∘ C ∘ K) = [False, False, True, True, False]"
"test (K ∘ C ∘ K ∘ C ∘ K ∘ C) = [False, True, True, True, True]"
"test (C ∘ K ∘ C ∘ K ∘ C ∘ K ∘ C) = [True, False, False, False, False]"
unfolding test_def C_def K_def
by (simp_all add: RRR_closure RRR_interior RRR_interior_closure closure_complement closed_interval_Int_compl o_apply)
(simp_all add: RRR_def)
theorem CK_nf_real_card:
shows "card ((λ f. f RRR) ` {f . CK_nf f}) = 14"
by (simp add: CK_nf_set) ((subst card_insert_disjoint; auto dest!: RRR_test simp: nf_RRR id_def[symmetric])[1])+
theorem CK_real_card:
shows "card {f::real set ⇒ real set. CK f} = 14" (is "?lhs = ?rhs")
proof(rule antisym[OF CK_card])
show "?rhs ≤ ?lhs"
unfolding CK_nf
by (rule le_trans[OF eq_imp_le[OF CK_nf_real_card[symmetric]] card_image_le])
(simp add: CK_nf_set)
qed
section‹ A corollary of Kuratowski's result \label{sec:kuratowski-corollary} ›
text‹
We show that it is a corollary of @{thm [source] CK_real_card} that at
most 7 distinct operators on a topological space can be generated by
compositions of closure and interior. In the case of
‹ℝ›, exactly 7 distinct operators can be so
generated.
›
inductive IK :: "('a::topological_space set ⇒ 'a set) ⇒ bool" where
"IK id"
| "IK I"
| "IK K"
| "⟦ IK f; IK g ⟧ ⟹ IK (f ∘ g)"
inductive IK_nf :: "('a::topological_space set ⇒ 'a set) ⇒ bool" where
"IK_nf id"
| "IK_nf I"
| "IK_nf K"
| "IK_nf (I ∘ K)"
| "IK_nf (K ∘ I)"
| "IK_nf (I ∘ K ∘ I)"
| "IK_nf (K ∘ I ∘ K)"
declare IK.intros[intro!]
declare IK_nf.intros[intro!]
lemma IK_nf_set:
"{f . IK_nf f} = {id, I, K, I ∘ K, K ∘ I, I ∘ K ∘ I, K ∘ I ∘ K}"
by (auto simp: IK_nf.simps)
theorem IK_nf:
"IK f ⟷ IK_nf f"
proof(rule iffI)
assume "IK f" then show "IK_nf f"
by induct
(elim IK_nf.cases; clarsimp simp: id_def[symmetric] o_assoc; simp add: I_I K_K o_assoc[symmetric]; clarsimp simp: K_I_K_I I_K_I_K o_assoc
| blast)+
next
assume "IK_nf f" then show "IK f" by induct blast+
qed
theorem IK_card:
shows "card {f. IK f} ≤ 7"
by (auto simp: IK_nf IK_nf_set card.insert_remove intro!: le_trans[OF card_Diff1_le])
theorem IK_nf_real_card:
shows "card ((λ f. f RRR) ` {f . IK_nf f}) = 7"
by (simp add: IK_nf_set) ((subst card_insert_disjoint; auto dest!: RRR_test simp: nf_RRR I_K id_def[symmetric] o_assoc)[1])+
theorem IK_real_card:
shows "card {f::real set ⇒ real set. IK f} = 7" (is "?lhs = ?rhs")
proof(rule antisym[OF IK_card])
show "?rhs ≤ ?lhs"
unfolding IK_nf
by (rule le_trans[OF eq_refl[OF IK_nf_real_card[symmetric]] card_image_le])
(simp add: IK_nf_set)
qed
section‹ Chagrov's result \label{sec:chagrov} ›
text‹
Chagrov's theorem, which is discussed in Section 2.1 of \<^cite>‹"GardnerJackson:2008"›, states that the number of distinct operators
on a topological space that can be generated by compositions of
closure and complement is one of 2, 6, 8, 10 or 14.
We begin by observing that the set of normal forms @{const "CK_nf"}
can be split into two disjoint sets, @{term "CK_nf_pos"} and @{term
"CK_nf_neg"}, which we define in terms of interior and closure.
›
inductive CK_nf_pos :: "('a::topological_space set ⇒ 'a set) ⇒ bool" where
"CK_nf_pos id"
| "CK_nf_pos I"
| "CK_nf_pos K"
| "CK_nf_pos (I ∘ K)"
| "CK_nf_pos (K ∘ I)"
| "CK_nf_pos (I ∘ K ∘ I)"
| "CK_nf_pos (K ∘ I ∘ K)"
declare CK_nf_pos.intros[intro!]
lemma CK_nf_pos_set:
shows "{f . CK_nf_pos f} = {id, I, K, I ∘ K, K ∘ I, I ∘ K ∘ I, K ∘ I ∘ K}"
by (auto simp: CK_nf_pos.simps)
definition
CK_nf_neg :: "('a::topological_space set ⇒ 'a set) ⇒ bool"
where
"CK_nf_neg f ⟷ (∃g. CK_nf_pos g ∧ f = C ∘ g)"
lemma CK_nf_pos_neg_disjoint:
assumes "CK_nf_pos f"
assumes "CK_nf_neg g"
shows "f ≠ g"
using assms unfolding CK_nf_neg_def
by (clarsimp simp: CK_nf_pos.simps; elim disjE; metis comp_def C_def I_def K_def Compl_iff closure_UNIV interior_UNIV id_apply)
lemma CK_nf_pos_neg_CK_nf:
"CK_nf f ⟷ CK_nf_pos f ∨ CK_nf_neg f" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
assume ?lhs then show ?rhs
unfolding CK_nf_neg_def
by (rule CK_nf.cases; metis (no_types, lifting) CK_nf_pos.simps C_C I_K K_I comp_id o_assoc)
next
assume ?rhs then show ?lhs
unfolding CK_nf_neg_def
by (auto elim!: CK_nf_pos.cases simp: I_K C_C o_assoc)
qed
text‹
We now focus on @{const "CK_nf_pos"}. In particular, we show that its
cardinality for any given topological space is one of 1, 3, 4, 5 or 7.
The proof consists of exhibiting normal forms for the operators
supported by each of six classes of topological spaces. These are
sublattices of the following lattice of @{const CK_nf_pos} operators:
›
lemmas K_I_K_subseteq_K = closure_mono[OF interior_subset, of "closure X", simplified] for X
lemma CK_nf_pos_lattice:
shows
"I ≤ (id :: 'a::topological_space set ⇒ 'a set)"
"id ≤ (K :: 'a::topological_space set ⇒ 'a set)"
"I ≤ I ∘ K ∘ (I :: 'a::topological_space set ⇒ 'a set)"
"I ∘ K ∘ I ≤ I ∘ (K :: 'a::topological_space set ⇒ 'a set)"
"I ∘ K ∘ I ≤ K ∘ (I :: 'a::topological_space set ⇒ 'a set)"
"I ∘ K ≤ K ∘ I ∘ (K :: 'a::topological_space set ⇒ 'a set)"
"K ∘ I ≤ K ∘ I ∘ (K :: 'a::topological_space set ⇒ 'a set)"
"K ∘ I ∘ K ≤ (K :: 'a::topological_space set ⇒ 'a set)"
unfolding I_def K_def
by (simp_all add: interior_subset closure_subset interior_maximal closure_mono o_apply interior_mono K_I_K_subseteq_K le_funI)
text‹
We define the six classes of topological spaces in question, and show
that they are related by inclusion in the following way (as shown in
Figure 2.3 of \<^cite>‹"GardnerJackson:2008"›):
\begin{center}
\begin{tikzpicture}[scale=.7]
\node (d) at (30:5cm) {Open unresolvable spaces};
\node (one) at (90:5cm) {Kuratowski spaces};
\node (b) at (150:5cm) {Extremally disconnected spaces};
\node (a) at (210:5cm) {Partition spaces};
\node (zero) at (270:5cm) {Discrete spaces};
\node (c) at (330:5cm) {\hspace{1cm}Extremally disconnected and open unresolvable spaces};
\draw (zero) -- (a) -- (b) -- (one) -- (d) -- (c) -- (zero);
\draw (c) -- (b);
\end{tikzpicture}
\end{center}
›
subsection‹ Discrete spaces ›
definition
"discrete (X :: 'a::topological_space set) ⟷ I = (id::'a set ⇒ 'a set)"
lemma discrete_eqs:
assumes "discrete (X :: 'a::topological_space set)"
shows
"I = (id::'a set ⇒ 'a set)"
"K = (id::'a set ⇒ 'a set)"
using assms unfolding discrete_def by (auto simp: C_C K_I)
lemma discrete_card:
assumes "discrete (X :: 'a::topological_space set)"
shows "card {f. CK_nf_pos (f::'a set ⇒ 'a set)} = 1"
using discrete_eqs[OF assms] CK_nf_pos_lattice[where 'a='a] by (simp add: CK_nf_pos_set)
lemma discrete_discrete_topology:
fixes X :: "'a::topological_space set"
assumes "⋀Y::'a set. open Y"
shows "discrete X"
using assms unfolding discrete_def I_def interior_def islimpt_def by (auto simp: fun_eq_iff)
subsection‹ Partition spaces ›
definition
"part (X :: 'a::topological_space set) ⟷ K ∘ I = (I :: 'a set ⇒ 'a set)"
lemma discrete_part:
assumes "discrete X"
shows "part X"
using assms unfolding discrete_def part_def by (simp add: C_C K_I)
lemma part_eqs:
assumes "part (X :: 'a::topological_space set)"
shows
"K ∘ I = (I :: 'a set ⇒ 'a set)"
"I ∘ K = (K :: 'a set ⇒ 'a set)"
using assms unfolding part_def by (assumption, metis (no_types, opaque_lifting) I_I K_I o_assoc)
lemma part_not_discrete_card:
assumes "part (X :: 'a::topological_space set)"
assumes "¬discrete X"
shows "card {f. CK_nf_pos (f::'a set ⇒ 'a set)} = 3"
using part_eqs[OF ‹part X›] ‹¬discrete X› CK_nf_pos_lattice[where 'a='a]
unfolding discrete_def
by (simp add: CK_nf_pos_set card_insert_if C_C I_K K_K o_assoc; metis comp_id)
text‹
A partition space is a topological space whose basis consists of the empty set and the equivalence classes of points of the space induced by some equivalence relation @{term "R"} on the underlying set of the space. Equivalently, a partition space is one in which every open set is closed. Thus, for example, the class of partition spaces includes every topological space whose open sets form a boolean algebra.
›