(* Author: L C Paulson, University of Cambridge [ported from HOL Light]
*)
section \<open>Operators involving abstract topology\<close>
theory Abstract_Topology
imports
Complex_Main
"HOL-Library.Set_Idioms"
"HOL-Library.FuncSet"
(* Path_Connected *)
begin
subsection \<open>General notion of a topology as a value\<close>
definition%important istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
"istopology L \<longleftrightarrow>
L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
morphisms "openin" "topology"
unfolding istopology_def by blast
lemma istopology_openin[intro]: "istopology(openin U)"
using openin[of U] by blast
lemma istopology_open: "istopology open"
by (auto simp: istopology_def)
lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
using topology_inverse[unfolded mem_Collect_eq] .
lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
using topology_inverse[of U] istopology_openin[of "topology U"] by auto
lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
proof
assume "T1 = T2"
then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp
next
assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
then have "openin T1 = openin T2" by (simp add: fun_eq_iff)
then have "topology (openin T1) = topology (openin T2)" by simp
then show "T1 = T2" unfolding openin_inverse .
qed
text\<open>The "universe": the union of all sets in the topology.\<close>
definition "topspace T = \<Union>{S. openin T S}"
subsubsection \<open>Main properties of open sets\<close>
proposition openin_clauses:
fixes U :: "'a topology"
shows
"openin U {}"
"\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
"\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
using openin[of U] unfolding istopology_def mem_Collect_eq by fast+
lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
unfolding topspace_def by blast
lemma openin_empty[simp]: "openin U {}"
by (rule openin_clauses)
lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
by (rule openin_clauses)
lemma openin_Union[intro]: "(\<And>S. S \<in> K \<Longrightarrow> openin U S) \<Longrightarrow> openin U (\<Union>K)"
using openin_clauses by blast
lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
using openin_Union[of "{S,T}" U] by auto
lemma openin_topspace[intro, simp]: "openin U (topspace U)"
by (force simp: openin_Union topspace_def)
lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs
then show ?rhs by auto
next
assume H: ?rhs
let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
have "openin U ?t" by (force simp: openin_Union)
also have "?t = S" using H by auto
finally show "openin U S" .
qed
lemma openin_INT [intro]:
assumes "finite I"
"\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
shows "openin T ((\<Inter>i \<in> I. U i) \<inter> topspace T)"
using assms by (induct, auto simp: inf_sup_aci(2) openin_Int)
lemma openin_INT2 [intro]:
assumes "finite I" "I \<noteq> {}"
"\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
shows "openin T (\<Inter>i \<in> I. U i)"
proof -
have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto
then show ?thesis
using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
qed
lemma openin_Inter [intro]:
assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
by (metis (full_types) assms openin_INT2 image_ident)
lemma openin_Int_Inter:
assumes "finite \<F>" "openin T U" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (U \<inter> \<Inter>\<F>)"
using openin_Inter [of "insert U \<F>"] assms by auto
subsubsection \<open>Closed sets\<close>
definition%important closedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
"closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
by (metis closedin_def)
lemma closedin_empty[simp]: "closedin U {}"
by (simp add: closedin_def)
lemma closedin_topspace[intro, simp]: "closedin U (topspace U)"
by (simp add: closedin_def)
lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
by (auto simp: Diff_Un closedin_def)
lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
by auto
lemma closedin_Union:
assumes "finite S" "\<And>T. T \<in> S \<Longrightarrow> closedin U T"
shows "closedin U (\<Union>S)"
using assms by induction auto
lemma closedin_Inter[intro]:
assumes Ke: "K \<noteq> {}"
and Kc: "\<And>S. S \<in>K \<Longrightarrow> closedin U S"
shows "closedin U (\<Inter>K)"
using Ke Kc unfolding closedin_def Diff_Inter by auto
lemma closedin_INT[intro]:
assumes "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> closedin U (B x)"
shows "closedin U (\<Inter>x\<in>A. B x)"
apply (rule closedin_Inter)
using assms
apply auto
done
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
using closedin_Inter[of "{S,T}" U] by auto
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
apply (auto simp: closedin_def Diff_Diff_Int inf_absorb2)
apply (metis openin_subset subset_eq)
done
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
by (simp add: openin_closedin_eq)
lemma openin_diff[intro]:
assumes oS: "openin U S"
and cT: "closedin U T"
shows "openin U (S - T)"
proof -
have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S] oS cT
by (auto simp: topspace_def openin_subset)
then show ?thesis using oS cT
by (auto simp: closedin_def)
qed
lemma closedin_diff[intro]:
assumes oS: "closedin U S"
and cT: "openin U T"
shows "closedin U (S - T)"
proof -
have "S - T = S \<inter> (topspace U - T)"
using closedin_subset[of U S] oS cT by (auto simp: topspace_def)
then show ?thesis
using oS cT by (auto simp: openin_closedin_eq)
qed
subsection\<open>The discrete topology\<close>
definition discrete_topology where "discrete_topology U \<equiv> topology (\<lambda>S. S \<subseteq> U)"
lemma openin_discrete_topology [simp]: "openin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
proof -
have "istopology (\<lambda>S. S \<subseteq> U)"
by (auto simp: istopology_def)
then show ?thesis
by (simp add: discrete_topology_def topology_inverse')
qed
lemma topspace_discrete_topology [simp]: "topspace(discrete_topology U) = U"
by (meson openin_discrete_topology openin_subset openin_topspace order_refl subset_antisym)
lemma closedin_discrete_topology [simp]: "closedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
by (simp add: closedin_def)
lemma discrete_topology_unique:
"discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> (\<forall>x \<in> U. openin X {x})" (is "?lhs = ?rhs")
proof
assume R: ?rhs
then have "openin X S" if "S \<subseteq> U" for S
using openin_subopen subsetD that by fastforce
moreover have "x \<in> topspace X" if "openin X S" and "x \<in> S" for x S
using openin_subset that by blast
ultimately
show ?lhs
using R by (auto simp: topology_eq)
qed auto
lemma discrete_topology_unique_alt:
"discrete_topology U = X \<longleftrightarrow> topspace X \<subseteq> U \<and> (\<forall>x \<in> U. openin X {x})"
using openin_subset
by (auto simp: discrete_topology_unique)
lemma subtopology_eq_discrete_topology_empty:
"X = discrete_topology {} \<longleftrightarrow> topspace X = {}"
using discrete_topology_unique [of "{}" X] by auto
lemma subtopology_eq_discrete_topology_sing:
"X = discrete_topology {a} \<longleftrightarrow> topspace X = {a}"
by (metis discrete_topology_unique openin_topspace singletonD)
subsection \<open>Subspace topology\<close>
definition%important subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a topology" where
"subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
(is "istopology ?L")
proof -
have "?L {}" by blast
{
fix A B
assume A: "?L A" and B: "?L B"
from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V"
by blast
have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"
using Sa Sb by blast+
then have "?L (A \<inter> B)" by blast
}
moreover
{
fix K
assume K: "K \<subseteq> Collect ?L"
have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
by blast
from K[unfolded th0 subset_image_iff]
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
by blast
have "\<Union>K = (\<Union>Sk) \<inter> V"
using Sk by auto
moreover have "openin U (\<Union>Sk)"
using Sk by (auto simp: subset_eq)
ultimately have "?L (\<Union>K)" by blast
}
ultimately show ?thesis
unfolding subset_eq mem_Collect_eq istopology_def by auto
qed
lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
by auto
lemma openin_subtopology_Int:
"openin X S \<Longrightarrow> openin (subtopology X T) (S \<inter> T)"
using openin_subtopology by auto
lemma openin_subtopology_Int2:
"openin X T \<Longrightarrow> openin (subtopology X S) (S \<inter> T)"
using openin_subtopology by auto
lemma openin_subtopology_diff_closed:
"\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> openin (subtopology X S) (S - T)"
unfolding closedin_def openin_subtopology
by (rule_tac x="topspace X - T" in exI) auto
lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)"
by (force simp: relative_to_def openin_subtopology)
lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
by (auto simp: topspace_def openin_subtopology)
lemma topspace_subtopology_subset:
"S \<subseteq> topspace X \<Longrightarrow> topspace(subtopology X S) = S"
by (simp add: inf.absorb_iff2 topspace_subtopology)
lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
unfolding closedin_def topspace_subtopology
by (auto simp: openin_subtopology)
lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
unfolding openin_subtopology
by auto (metis IntD1 in_mono openin_subset)
lemma subtopology_subtopology:
"subtopology (subtopology X S) T = subtopology X (S \<inter> T)"
proof -
have eq: "\<And>T'. (\<exists>S'. T' = S' \<inter> T \<and> (\<exists>T. openin X T \<and> S' = T \<inter> S)) = (\<exists>Sa. T' = Sa \<inter> (S \<inter> T) \<and> openin X Sa)"
by (metis inf_assoc)
have "subtopology (subtopology X S) T = topology (\<lambda>Ta. \<exists>Sa. Ta = Sa \<inter> T \<and> openin (subtopology X S) Sa)"
by (simp add: subtopology_def)
also have "\<dots> = subtopology X (S \<inter> T)"
by (simp add: openin_subtopology eq) (simp add: subtopology_def)
finally show ?thesis .
qed
lemma openin_subtopology_alt:
"openin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (openin X)"
by (simp add: image_iff inf_commute openin_subtopology)
lemma closedin_subtopology_alt:
"closedin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (closedin X)"
by (simp add: image_iff inf_commute closedin_subtopology)
lemma subtopology_superset:
assumes UV: "topspace U \<subseteq> V"
shows "subtopology U V = U"
proof -
{
fix S
{
fix T
assume T: "openin U T" "S = T \<inter> V"
from T openin_subset[OF T(1)] UV have eq: "S = T"
by blast
have "openin U S"
unfolding eq using T by blast
}
moreover
{
assume S: "openin U S"
then have "\<exists>T. openin U T \<and> S = T \<inter> V"
using openin_subset[OF S] UV by auto
}
ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S"
by blast
}
then show ?thesis
unfolding topology_eq openin_subtopology by blast
qed
lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
by (simp add: subtopology_superset)
lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
by (simp add: subtopology_superset)
lemma subtopology_restrict:
"subtopology X (topspace X \<inter> S) = subtopology X S"
by (metis subtopology_subtopology subtopology_topspace)
lemma openin_subtopology_empty:
"openin (subtopology U {}) S \<longleftrightarrow> S = {}"
by (metis Int_empty_right openin_empty openin_subtopology)
lemma closedin_subtopology_empty:
"closedin (subtopology U {}) S \<longleftrightarrow> S = {}"
by (metis Int_empty_right closedin_empty closedin_subtopology)
lemma closedin_subtopology_refl [simp]:
"closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
by (simp add: closedin_def)
lemma openin_imp_subset:
"openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
by (metis Int_iff openin_subtopology subsetI)
lemma closedin_imp_subset:
"closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
by (simp add: closedin_def topspace_subtopology)
lemma openin_open_subtopology:
"openin X S \<Longrightarrow> openin (subtopology X S) T \<longleftrightarrow> openin X T \<and> T \<subseteq> S"
by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology)
lemma closedin_closed_subtopology:
"closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)
lemma openin_subtopology_Un:
"\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
\<Longrightarrow> openin (subtopology X (T \<union> U)) S"
by (simp add: openin_subtopology) blast
lemma closedin_subtopology_Un:
"\<lbrakk>closedin (subtopology X T) S; closedin (subtopology X U) S\<rbrakk>
\<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
by (simp add: closedin_subtopology) blast
subsection \<open>The standard Euclidean topology\<close>
abbreviation%important euclidean :: "'a::topological_space topology"
where "euclidean \<equiv> topology open"
abbreviation top_of_set :: "'a::topological_space set \<Rightarrow> 'a topology"
where "top_of_set \<equiv> subtopology (topology open)"
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
apply (rule cong[where x=S and y=S])
apply (rule topology_inverse[symmetric])
apply (auto simp: istopology_def)
done
declare open_openin [symmetric, simp]
lemma topspace_euclidean [simp]: "topspace euclidean = UNIV"
by (force simp: topspace_def)
lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S"
by (simp add: topspace_subtopology)
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)
declare closed_closedin [symmetric, simp]
lemma openin_subtopology_self [simp]: "openin (subtopology euclidean S) S"
by (metis openin_topspace topspace_euclidean_subtopology)
subsubsection\<open>The most basic facts about the usual topology and metric on R\<close>
abbreviation euclideanreal :: "real topology"
where "euclideanreal \<equiv> topology open"
subsection \<open>Basic "localization" results are handy for connectedness.\<close>
lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
by (auto simp: openin_subtopology)
lemma openin_Int_open:
"\<lbrakk>openin (subtopology euclidean U) S; open T\<rbrakk>
\<Longrightarrow> openin (subtopology euclidean U) (S \<inter> T)"
by (metis open_Int Int_assoc openin_open)
lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)"
by (auto simp: openin_open)
lemma open_openin_trans[trans]:
"open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
by (metis Int_absorb1 openin_open_Int)
lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
by (auto simp: openin_open)
lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
by (simp add: closedin_subtopology Int_ac)
lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> S)"
by (metis closedin_closed)
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
by (auto simp: closedin_closed)
lemma closedin_closed_subset:
"\<lbrakk>closedin (subtopology euclidean U) V; T \<subseteq> U; S = V \<inter> T\<rbrakk>
\<Longrightarrow> closedin (subtopology euclidean T) S"
by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE)
lemma finite_imp_closedin:
fixes S :: "'a::t1_space set"
shows "\<lbrakk>finite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology euclidean T) S"
by (simp add: finite_imp_closed closed_subset)
lemma closedin_singleton [simp]:
fixes a :: "'a::t1_space"
shows "closedin (subtopology euclidean U) {a} \<longleftrightarrow> a \<in> U"
using closedin_subset by (force intro: closed_subset)
lemma openin_euclidean_subtopology_iff:
fixes S U :: "'a::metric_space set"
shows "openin (subtopology euclidean U) S \<longleftrightarrow>
S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs
then show ?rhs
unfolding openin_open open_dist by blast
next
define T where "T = {x. \<exists>a\<in>S. \<exists>d>0. (\<forall>y\<in>U. dist y a < d \<longrightarrow> y \<in> S) \<and> dist x a < d}"
have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
unfolding T_def
apply clarsimp
apply (rule_tac x="d - dist x a" in exI)
apply (clarsimp simp add: less_diff_eq)
by (metis dist_commute dist_triangle_lt)
assume ?rhs then have 2: "S = U \<inter> T"
unfolding T_def
by auto (metis dist_self)
from 1 2 show ?lhs
unfolding openin_open open_dist by fast
qed
lemma connected_openin:
"connected S \<longleftrightarrow>
\<not>(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
openin (subtopology euclidean S) E2 \<and>
S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
by (simp_all, blast+) (* SLOW *)
lemma connected_openin_eq:
"connected S \<longleftrightarrow>
\<not>(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
openin (subtopology euclidean S) E2 \<and>
E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
E1 \<noteq> {} \<and> E2 \<noteq> {})"
apply (simp add: connected_openin, safe, blast)
by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)
lemma connected_closedin:
"connected S \<longleftrightarrow>
(\<nexists>E1 E2.
closedin (subtopology euclidean S) E1 \<and>
closedin (subtopology euclidean S) E2 \<and>
S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (auto simp add: connected_closed closedin_closed)
next
assume R: ?rhs
then show ?lhs
proof (clarsimp simp add: connected_closed closedin_closed)
fix A B
assume s_sub: "S \<subseteq> A \<union> B" "B \<inter> S \<noteq> {}"
and disj: "A \<inter> B \<inter> S = {}"
and cl: "closed A" "closed B"
have "S \<inter> (A \<union> B) = S"
using s_sub(1) by auto
have "S - A = B \<inter> S"
using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto
then have "S \<inter> A = {}"
by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int R cl closedin_closed_Int inf_commute order_refl s_sub(2))
then show "A \<inter> S = {}"
by blast
qed
qed
lemma connected_closedin_eq:
"connected S \<longleftrightarrow>
\<not>(\<exists>E1 E2.
closedin (subtopology euclidean S) E1 \<and>
closedin (subtopology euclidean S) E2 \<and>
E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
E1 \<noteq> {} \<and> E2 \<noteq> {})"
apply (simp add: connected_closedin, safe, blast)
by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)
text \<open>These "transitivity" results are handy too\<close>
lemma openin_trans[trans]:
"openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow>
openin (subtopology euclidean U) S"
by (metis openin_Int_open openin_open)
lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S"
by (auto simp: openin_open intro: openin_trans)
lemma closedin_trans[trans]:
"closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow>
closedin (subtopology euclidean U) S"
by (auto simp: closedin_closed closed_Inter Int_assoc)
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
by (auto simp: closedin_closed intro: closedin_trans)
lemma openin_subtopology_Int_subset:
"\<lbrakk>openin (subtopology euclidean u) (u \<inter> S); v \<subseteq> u\<rbrakk> \<Longrightarrow> openin (subtopology euclidean v) (v \<inter> S)"
by (auto simp: openin_subtopology)
lemma openin_open_eq: "open s \<Longrightarrow> (openin (subtopology euclidean s) t \<longleftrightarrow> open t \<and> t \<subseteq> s)"
using open_subset openin_open_trans openin_subset by fastforce
subsection\<open>Derived set (set of limit points)\<close>
definition derived_set_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "derived'_set'_of" 80)
where "X derived_set_of S \<equiv>
{x \<in> topspace X.
(\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))}"
lemma derived_set_of_restrict:
"X derived_set_of (topspace X \<inter> S) = X derived_set_of S"
by (simp add: derived_set_of_def) (metis openin_subset subset_iff)
lemma in_derived_set_of:
"x \<in> X derived_set_of S \<longleftrightarrow> x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))"
by (simp add: derived_set_of_def)
lemma derived_set_of_subset_topspace:
"X derived_set_of S \<subseteq> topspace X"
by (auto simp add: derived_set_of_def)
lemma derived_set_of_subtopology:
"(subtopology X U) derived_set_of S = U \<inter> (X derived_set_of (U \<inter> S))"
by (simp add: derived_set_of_def openin_subtopology topspace_subtopology) blast
lemma derived_set_of_subset_subtopology:
"(subtopology X S) derived_set_of T \<subseteq> S"
by (simp add: derived_set_of_subtopology)
lemma derived_set_of_empty [simp]: "X derived_set_of {} = {}"
by (auto simp: derived_set_of_def)
lemma derived_set_of_mono:
"S \<subseteq> T \<Longrightarrow> X derived_set_of S \<subseteq> X derived_set_of T"
unfolding derived_set_of_def by blast
lemma derived_set_of_union:
"X derived_set_of (S \<union> T) = X derived_set_of S \<union> X derived_set_of T" (is "?lhs = ?rhs")
proof
show "?lhs \<subseteq> ?rhs"
apply (clarsimp simp: in_derived_set_of)
by (metis IntE IntI openin_Int)
show "?rhs \<subseteq> ?lhs"
by (simp add: derived_set_of_mono)
qed
lemma derived_set_of_unions:
"finite \<F> \<Longrightarrow> X derived_set_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X derived_set_of S)"
proof (induction \<F> rule: finite_induct)
case (insert S \<F>)
then show ?case
by (simp add: derived_set_of_union)
qed auto
lemma derived_set_of_topspace:
"X derived_set_of (topspace X) = {x \<in> topspace X. \<not> openin X {x}}"
apply (auto simp: in_derived_set_of)
by (metis Set.set_insert all_not_in_conv insertCI openin_subset subsetCE)
lemma discrete_topology_unique_derived_set:
"discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> X derived_set_of U = {}"
by (auto simp: discrete_topology_unique derived_set_of_topspace)
lemma subtopology_eq_discrete_topology_eq:
"subtopology X U = discrete_topology U \<longleftrightarrow> U \<subseteq> topspace X \<and> U \<inter> X derived_set_of U = {}"
using discrete_topology_unique_derived_set [of U "subtopology X U"]
by (auto simp: eq_commute topspace_subtopology derived_set_of_subtopology)
lemma subtopology_eq_discrete_topology:
"S \<subseteq> topspace X \<and> S \<inter> X derived_set_of S = {}
\<Longrightarrow> subtopology X S = discrete_topology S"
by (simp add: subtopology_eq_discrete_topology_eq)
lemma subtopology_eq_discrete_topology_gen:
"S \<inter> X derived_set_of S = {} \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
by (metis Int_lower1 derived_set_of_restrict inf_assoc inf_bot_right subtopology_eq_discrete_topology_eq subtopology_subtopology subtopology_topspace)
lemma subtopology_discrete_topology [simp]: "subtopology (discrete_topology U) S = discrete_topology(U \<inter> S)"
proof -
have "(\<lambda>T. \<exists>Sa. T = Sa \<inter> S \<and> Sa \<subseteq> U) = (\<lambda>Sa. Sa \<subseteq> U \<and> Sa \<subseteq> S)"
by force
then show ?thesis
by (simp add: subtopology_def) (simp add: discrete_topology_def)
qed
lemma openin_Int_derived_set_of_subset:
"openin X S \<Longrightarrow> S \<inter> X derived_set_of T \<subseteq> X derived_set_of (S \<inter> T)"
by (auto simp: derived_set_of_def)
lemma openin_Int_derived_set_of_eq:
"openin X S \<Longrightarrow> S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
apply auto
apply (meson IntI openin_Int_derived_set_of_subset subsetCE)
by (meson derived_set_of_mono inf_sup_ord(2) subset_eq)
subsection\<open> Closure with respect to a topological space\<close>
definition closure_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "closure'_of" 80)
where "X closure_of S \<equiv> {x \<in> topspace X. \<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y \<in> S. y \<in> T)}"
lemma closure_of_restrict: "X closure_of S = X closure_of (topspace X \<inter> S)"
unfolding closure_of_def
apply safe
apply (meson IntI openin_subset subset_iff)
by auto
lemma in_closure_of:
"x \<in> X closure_of S \<longleftrightarrow>
x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<in> S \<and> y \<in> T))"
by (auto simp: closure_of_def)
lemma closure_of: "X closure_of S = topspace X \<inter> (S \<union> X derived_set_of S)"
by (fastforce simp: in_closure_of in_derived_set_of)
lemma closure_of_alt: "X closure_of S = topspace X \<inter> S \<union> X derived_set_of S"
using derived_set_of_subset_topspace [of X S]
unfolding closure_of_def in_derived_set_of
by safe (auto simp: in_derived_set_of)
lemma derived_set_of_subset_closure_of:
"X derived_set_of S \<subseteq> X closure_of S"
by (fastforce simp: closure_of_def in_derived_set_of)
lemma closure_of_subtopology:
"(subtopology X U) closure_of S = U \<inter> (X closure_of (U \<inter> S))"
unfolding closure_of_def topspace_subtopology openin_subtopology
by safe (metis (full_types) IntI Int_iff inf.commute)+
lemma closure_of_empty [simp]: "X closure_of {} = {}"
by (simp add: closure_of_alt)
lemma closure_of_topspace [simp]: "X closure_of topspace X = topspace X"
by (simp add: closure_of)
lemma closure_of_UNIV [simp]: "X closure_of UNIV = topspace X"
by (simp add: closure_of)
lemma closure_of_subset_topspace: "X closure_of S \<subseteq> topspace X"
by (simp add: closure_of)
lemma closure_of_subset_subtopology: "(subtopology X S) closure_of T \<subseteq> S"
by (simp add: closure_of_subtopology)
lemma closure_of_mono: "S \<subseteq> T \<Longrightarrow> X closure_of S \<subseteq> X closure_of T"
by (fastforce simp add: closure_of_def)
lemma closure_of_subtopology_subset:
"(subtopology X U) closure_of S \<subseteq> (X closure_of S)"
unfolding closure_of_subtopology
by clarsimp (meson closure_of_mono contra_subsetD inf.cobounded2)
lemma closure_of_subtopology_mono:
"T \<subseteq> U \<Longrightarrow> (subtopology X T) closure_of S \<subseteq> (subtopology X U) closure_of S"
unfolding closure_of_subtopology
by auto (meson closure_of_mono inf_mono subset_iff)
lemma closure_of_Un [simp]: "X closure_of (S \<union> T) = X closure_of S \<union> X closure_of T"
by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_union inf_sup_distrib1)
lemma closure_of_Union:
"finite \<F> \<Longrightarrow> X closure_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X closure_of S)"
by (induction \<F> rule: finite_induct) auto
lemma closure_of_subset: "S \<subseteq> topspace X \<Longrightarrow> S \<subseteq> X closure_of S"
by (auto simp: closure_of_def)
lemma closure_of_subset_Int: "topspace X \<inter> S \<subseteq> X closure_of S"
by (auto simp: closure_of_def)
lemma closure_of_subset_eq: "S \<subseteq> topspace X \<and> X closure_of S \<subseteq> S \<longleftrightarrow> closedin X S"
proof (cases "S \<subseteq> topspace X")
case True
then have "\<forall>x. x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<in>S. y \<in> T)) \<longrightarrow> x \<in> S
\<Longrightarrow> openin X (topspace X - S)"
apply (subst openin_subopen, safe)
by (metis DiffI subset_eq openin_subset [of X])
then show ?thesis
by (auto simp: closedin_def closure_of_def)
next
case False
then show ?thesis
by (simp add: closedin_def)
qed
lemma closure_of_eq: "X closure_of S = S \<longleftrightarrow> closedin X S"
proof (cases "S \<subseteq> topspace X")
case True
then show ?thesis
by (metis closure_of_subset closure_of_subset_eq set_eq_subset)
next
case False
then show ?thesis
using closure_of closure_of_subset_eq by fastforce
qed
lemma closedin_contains_derived_set:
"closedin X S \<longleftrightarrow> X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X"
proof (intro iffI conjI)
show "closedin X S \<Longrightarrow> X derived_set_of S \<subseteq> S"
using closure_of_eq derived_set_of_subset_closure_of by fastforce
show "closedin X S \<Longrightarrow> S \<subseteq> topspace X"
using closedin_subset by blast
show "X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X \<Longrightarrow> closedin X S"
by (metis closure_of closure_of_eq inf.absorb_iff2 sup.orderE)
qed
lemma derived_set_subset_gen:
"X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X (topspace X \<inter> S)"
by (simp add: closedin_contains_derived_set derived_set_of_restrict derived_set_of_subset_topspace)
lemma derived_set_subset: "S \<subseteq> topspace X \<Longrightarrow> (X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X S)"
by (simp add: closedin_contains_derived_set)
lemma closedin_derived_set:
"closedin (subtopology X T) S \<longleftrightarrow>
S \<subseteq> topspace X \<and> S \<subseteq> T \<and> (\<forall>x. x \<in> X derived_set_of S \<and> x \<in> T \<longrightarrow> x \<in> S)"
by (auto simp: closedin_contains_derived_set topspace_subtopology derived_set_of_subtopology Int_absorb1)
lemma closedin_Int_closure_of:
"closedin (subtopology X S) T \<longleftrightarrow> S \<inter> X closure_of T = T"
by (metis Int_left_absorb closure_of_eq closure_of_subtopology)
lemma closure_of_closedin: "closedin X S \<Longrightarrow> X closure_of S = S"
by (simp add: closure_of_eq)
lemma closure_of_eq_diff: "X closure_of S = topspace X - \<Union>{T. openin X T \<and> disjnt S T}"
by (auto simp: closure_of_def disjnt_iff)
lemma closedin_closure_of [simp]: "closedin X (X closure_of S)"
unfolding closure_of_eq_diff by blast
lemma closure_of_closure_of [simp]: "X closure_of (X closure_of S) = X closure_of S"
by (simp add: closure_of_eq)
lemma closure_of_hull:
assumes "S \<subseteq> topspace X" shows "X closure_of S = (closedin X) hull S"
proof (rule hull_unique [THEN sym])
show "S \<subseteq> X closure_of S"
by (simp add: closure_of_subset assms)
next
show "closedin X (X closure_of S)"
by simp
show "\<And>T. \<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> X closure_of S \<subseteq> T"
by (metis closure_of_eq closure_of_mono)
qed
lemma closure_of_minimal:
"\<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T"
by (metis closure_of_eq closure_of_mono)
lemma closure_of_minimal_eq:
"\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T \<longleftrightarrow> S \<subseteq> T"
by (meson closure_of_minimal closure_of_subset subset_trans)
lemma closure_of_unique:
"\<lbrakk>S \<subseteq> T; closedin X T;
\<And>T'. \<lbrakk>S \<subseteq> T'; closedin X T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk>
\<Longrightarrow> X closure_of S = T"
by (meson closedin_closure_of closedin_subset closure_of_minimal closure_of_subset eq_iff order.trans)
lemma closure_of_eq_empty_gen: "X closure_of S = {} \<longleftrightarrow> disjnt (topspace X) S"
unfolding disjnt_def closure_of_restrict [where S=S]
using closure_of by fastforce
lemma closure_of_eq_empty: "S \<subseteq> topspace X \<Longrightarrow> X closure_of S = {} \<longleftrightarrow> S = {}"
using closure_of_subset by fastforce
lemma openin_Int_closure_of_subset:
assumes "openin X S"
shows "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
proof -
have "S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
by (meson assms openin_Int_derived_set_of_eq)
moreover have "S \<inter> (S \<inter> T) = S \<inter> T"
by fastforce
ultimately show ?thesis
by (metis closure_of_alt inf.cobounded2 inf_left_commute inf_sup_distrib1)
qed
lemma closure_of_openin_Int_closure_of:
assumes "openin X S"
shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)"
proof
show "X closure_of (S \<inter> X closure_of T) \<subseteq> X closure_of (S \<inter> T)"
by (simp add: assms closure_of_minimal openin_Int_closure_of_subset)
next
show "X closure_of (S \<inter> T) \<subseteq> X closure_of (S \<inter> X closure_of T)"
by (metis Int_lower1 Int_subset_iff assms closedin_closure_of closure_of_minimal_eq closure_of_mono inf_le2 le_infI1 openin_subset)
qed
lemma openin_Int_closure_of_eq:
"openin X S \<Longrightarrow> S \<inter> X closure_of T = S \<inter> X closure_of (S \<inter> T)"
apply (rule equalityI)
apply (simp add: openin_Int_closure_of_subset)
by (meson closure_of_mono inf.cobounded2 inf_mono subset_refl)
lemma openin_Int_closure_of_eq_empty:
"openin X S \<Longrightarrow> S \<inter> X closure_of T = {} \<longleftrightarrow> S \<inter> T = {}"
apply (subst openin_Int_closure_of_eq, auto)
by (meson IntI closure_of_subset_Int disjoint_iff_not_equal openin_subset subset_eq)
lemma closure_of_openin_Int_superset:
"openin X S \<and> S \<subseteq> X closure_of T
\<Longrightarrow> X closure_of (S \<inter> T) = X closure_of S"
by (metis closure_of_openin_Int_closure_of inf.orderE)
lemma closure_of_openin_subtopology_Int_closure_of:
assumes S: "openin (subtopology X U) S" and "T \<subseteq> U"
shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)" (is "?lhs = ?rhs")
proof
obtain S0 where S0: "openin X S0" "S = S0 \<inter> U"
using assms by (auto simp: openin_subtopology)
show "?lhs \<subseteq> ?rhs"
proof -
have "S0 \<inter> X closure_of T = S0 \<inter> X closure_of (S0 \<inter> T)"
by (meson S0(1) openin_Int_closure_of_eq)
moreover have "S0 \<inter> T = S0 \<inter> U \<inter> T"
using \<open>T \<subseteq> U\<close> by fastforce
ultimately have "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
using S0(2) by auto
then show ?thesis
by (meson closedin_closure_of closure_of_minimal)
qed
next
show "?rhs \<subseteq> ?lhs"
proof -
have "T \<inter> S \<subseteq> T \<union> X derived_set_of T"
by force
then show ?thesis
by (metis Int_subset_iff S closure_of closure_of_mono inf.cobounded2 inf.coboundedI2 inf_commute openin_closedin_eq topspace_subtopology)
qed
qed
lemma closure_of_subtopology_open:
"openin X U \<or> S \<subseteq> U \<Longrightarrow> (subtopology X U) closure_of S = U \<inter> X closure_of S"
by (metis closure_of_subtopology inf_absorb2 openin_Int_closure_of_eq)
lemma discrete_topology_closure_of:
"(discrete_topology U) closure_of S = U \<inter> S"
by (metis closedin_discrete_topology closure_of_restrict closure_of_unique discrete_topology_unique inf_sup_ord(1) order_refl)
text\<open> Interior with respect to a topological space. \<close>
definition interior_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "interior'_of" 80)
where "X interior_of S \<equiv> {x. \<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> S}"
lemma interior_of_restrict:
"X interior_of S = X interior_of (topspace X \<inter> S)"
using openin_subset by (auto simp: interior_of_def)
lemma interior_of_eq: "(X interior_of S = S) \<longleftrightarrow> openin X S"
unfolding interior_of_def using openin_subopen by blast
lemma interior_of_openin: "openin X S \<Longrightarrow> X interior_of S = S"
by (simp add: interior_of_eq)
lemma interior_of_empty [simp]: "X interior_of {} = {}"
by (simp add: interior_of_eq)
lemma interior_of_topspace [simp]: "X interior_of (topspace X) = topspace X"
by (simp add: interior_of_eq)
lemma openin_interior_of [simp]: "openin X (X interior_of S)"
unfolding interior_of_def
using openin_subopen by fastforce
lemma interior_of_interior_of [simp]:
"X interior_of X interior_of S = X interior_of S"
by (simp add: interior_of_eq)
lemma interior_of_subset: "X interior_of S \<subseteq> S"
by (auto simp: interior_of_def)
lemma interior_of_subset_closure_of: "X interior_of S \<subseteq> X closure_of S"
by (metis closure_of_subset_Int dual_order.trans interior_of_restrict interior_of_subset)
lemma subset_interior_of_eq: "S \<subseteq> X interior_of S \<longleftrightarrow> openin X S"
by (metis interior_of_eq interior_of_subset subset_antisym)
lemma interior_of_mono: "S \<subseteq> T \<Longrightarrow> X interior_of S \<subseteq> X interior_of T"
by (auto simp: interior_of_def)
lemma interior_of_maximal: "\<lbrakk>T \<subseteq> S; openin X T\<rbrakk> \<Longrightarrow> T \<subseteq> X interior_of S"
by (auto simp: interior_of_def)
lemma interior_of_maximal_eq: "openin X T \<Longrightarrow> T \<subseteq> X interior_of S \<longleftrightarrow> T \<subseteq> S"
by (meson interior_of_maximal interior_of_subset order_trans)
lemma interior_of_unique:
"\<lbrakk>T \<subseteq> S; openin X T; \<And>T'. \<lbrakk>T' \<subseteq> S; openin X T'\<rbrakk> \<Longrightarrow> T' \<subseteq> T\<rbrakk> \<Longrightarrow> X interior_of S = T"
by (simp add: interior_of_maximal_eq interior_of_subset subset_antisym)
lemma interior_of_subset_topspace: "X interior_of S \<subseteq> topspace X"
by (simp add: openin_subset)
lemma interior_of_subset_subtopology: "(subtopology X S) interior_of T \<subseteq> S"
by (meson openin_imp_subset openin_interior_of)
lemma interior_of_Int: "X interior_of (S \<inter> T) = X interior_of S \<inter> X interior_of T"
apply (rule equalityI)
apply (simp add: interior_of_mono)
apply (auto simp: interior_of_maximal_eq openin_Int interior_of_subset le_infI1 le_infI2)
done
lemma interior_of_Inter_subset: "X interior_of (\<Inter>\<F>) \<subseteq> (\<Inter>S \<in> \<F>. X interior_of S)"
by (simp add: INT_greatest Inf_lower interior_of_mono)
lemma union_interior_of_subset:
"X interior_of S \<union> X interior_of T \<subseteq> X interior_of (S \<union> T)"
by (simp add: interior_of_mono)
lemma interior_of_eq_empty:
"X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<subseteq> S \<longrightarrow> T = {})"
by (metis bot.extremum_uniqueI interior_of_maximal interior_of_subset openin_interior_of)
lemma interior_of_eq_empty_alt:
"X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> T - S \<noteq> {})"
by (auto simp: interior_of_eq_empty)
lemma interior_of_Union_openin_subsets:
"\<Union>{T. openin X T \<and> T \<subseteq> S} = X interior_of S"
by (rule interior_of_unique [symmetric]) auto
lemma interior_of_complement:
"X interior_of (topspace X - S) = topspace X - X closure_of S"
by (auto simp: interior_of_def closure_of_def)
lemma interior_of_closure_of:
"X interior_of S = topspace X - X closure_of (topspace X - S)"
unfolding interior_of_complement [symmetric]
by (metis Diff_Diff_Int interior_of_restrict)
lemma closure_of_interior_of:
"X closure_of S = topspace X - X interior_of (topspace X - S)"
by (simp add: interior_of_complement Diff_Diff_Int closure_of)
lemma closure_of_complement: "X closure_of (topspace X - S) = topspace X - X interior_of S"
unfolding interior_of_def closure_of_def
by (blast dest: openin_subset)
lemma interior_of_eq_empty_complement:
"X interior_of S = {} \<longleftrightarrow> X closure_of (topspace X - S) = topspace X"
using interior_of_subset_topspace [of X S] closure_of_complement by fastforce
lemma closure_of_eq_topspace:
"X closure_of S = topspace X \<longleftrightarrow> X interior_of (topspace X - S) = {}"
using closure_of_subset_topspace [of X S] interior_of_complement by fastforce
lemma interior_of_subtopology_subset:
"U \<inter> X interior_of S \<subseteq> (subtopology X U) interior_of S"
by (auto simp: interior_of_def openin_subtopology)
lemma interior_of_subtopology_subsets:
"T \<subseteq> U \<Longrightarrow> T \<inter> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
by (metis inf.absorb_iff2 interior_of_subtopology_subset subtopology_subtopology)
lemma interior_of_subtopology_mono:
"\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
by (metis dual_order.trans inf.orderE inf_commute interior_of_subset interior_of_subtopology_subsets)
lemma interior_of_subtopology_open:
assumes "openin X U"
shows "(subtopology X U) interior_of S = U \<inter> X interior_of S"
proof -
have "\<forall>A. U \<inter> X closure_of (U \<inter> A) = U \<inter> X closure_of A"
using assms openin_Int_closure_of_eq by blast
then have "topspace X \<inter> U - U \<inter> X closure_of (topspace X \<inter> U - S) = U \<inter> (topspace X - X closure_of (topspace X - S))"
by (metis (no_types) Diff_Int_distrib Int_Diff inf_commute)
then show ?thesis
unfolding interior_of_closure_of closure_of_subtopology_open topspace_subtopology
using openin_Int_closure_of_eq [OF assms]
by (metis assms closure_of_subtopology_open)
qed
lemma dense_intersects_open:
"X closure_of S = topspace X \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
proof -
have "X closure_of S = topspace X \<longleftrightarrow> (topspace X - X interior_of (topspace X - S) = topspace X)"
by (simp add: closure_of_interior_of)
also have "\<dots> \<longleftrightarrow> X interior_of (topspace X - S) = {}"
by (simp add: closure_of_complement interior_of_eq_empty_complement)
also have "\<dots> \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
unfolding interior_of_eq_empty_alt
using openin_subset by fastforce
finally show ?thesis .
qed
lemma interior_of_closedin_union_empty_interior_of:
assumes "closedin X S" and disj: "X interior_of T = {}"
shows "X interior_of (S \<union> T) = X interior_of S"
proof -
have "X closure_of (topspace X - T) = topspace X"
by (metis Diff_Diff_Int disj closure_of_eq_topspace closure_of_restrict interior_of_closure_of)
then show ?thesis
unfolding interior_of_closure_of
by (metis Diff_Un Diff_subset assms(1) closedin_def closure_of_openin_Int_superset)
qed
lemma interior_of_union_eq_empty:
"closedin X S
\<Longrightarrow> (X interior_of (S \<union> T) = {} \<longleftrightarrow>
X interior_of S = {} \<and> X interior_of T = {})"
by (metis interior_of_closedin_union_empty_interior_of le_sup_iff subset_empty union_interior_of_subset)
lemma discrete_topology_interior_of [simp]:
"(discrete_topology U) interior_of S = U \<inter> S"
by (simp add: interior_of_restrict [of _ S] interior_of_eq)
subsection \<open>Frontier with respect to topological space \<close>
definition frontier_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "frontier'_of" 80)
where "X frontier_of S \<equiv> X closure_of S - X interior_of S"
lemma frontier_of_closures:
"X frontier_of S = X closure_of S \<inter> X closure_of (topspace X - S)"
by (metis Diff_Diff_Int closure_of_complement closure_of_subset_topspace double_diff frontier_of_def interior_of_subset_closure_of)
lemma interior_of_union_frontier_of [simp]:
"X interior_of S \<union> X frontier_of S = X closure_of S"
by (simp add: frontier_of_def interior_of_subset_closure_of subset_antisym)
lemma frontier_of_restrict: "X frontier_of S = X frontier_of (topspace X \<inter> S)"
by (metis closure_of_restrict frontier_of_def interior_of_restrict)
lemma closedin_frontier_of: "closedin X (X frontier_of S)"
by (simp add: closedin_Int frontier_of_closures)
lemma frontier_of_subset_topspace: "X frontier_of S \<subseteq> topspace X"
by (simp add: closedin_frontier_of closedin_subset)
lemma frontier_of_subset_subtopology: "(subtopology X S) frontier_of T \<subseteq> S"
by (metis (no_types) closedin_derived_set closedin_frontier_of)
lemma frontier_of_subtopology_subset:
"U \<inter> (subtopology X U) frontier_of S \<subseteq> (X frontier_of S)"
proof -
have "U \<inter> X interior_of S - subtopology X U interior_of S = {}"
by (simp add: interior_of_subtopology_subset)
moreover have "X closure_of S \<inter> subtopology X U closure_of S = subtopology X U closure_of S"
by (meson closure_of_subtopology_subset inf.absorb_iff2)
ultimately show ?thesis
unfolding frontier_of_def
by blast
qed
lemma frontier_of_subtopology_mono:
"\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X T) frontier_of S \<subseteq> (subtopology X U) frontier_of S"
by (simp add: frontier_of_def Diff_mono closure_of_subtopology_mono interior_of_subtopology_mono)
lemma clopenin_eq_frontier_of:
"closedin X S \<and> openin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> X frontier_of S = {}"
proof (cases "S \<subseteq> topspace X")
case True
then show ?thesis
by (metis Diff_eq_empty_iff closure_of_eq closure_of_subset_eq frontier_of_def interior_of_eq interior_of_subset interior_of_union_frontier_of sup_bot_right)
next
case False
then show ?thesis
by (simp add: frontier_of_closures openin_closedin_eq)
qed
lemma frontier_of_eq_empty:
"S \<subseteq> topspace X \<Longrightarrow> (X frontier_of S = {} \<longleftrightarrow> closedin X S \<and> openin X S)"
by (simp add: clopenin_eq_frontier_of)
lemma frontier_of_openin:
"openin X S \<Longrightarrow> X frontier_of S = X closure_of S - S"
by (metis (no_types) frontier_of_def interior_of_eq)
lemma frontier_of_openin_straddle_Int:
assumes "openin X U" "U \<inter> X frontier_of S \<noteq> {}"
shows "U \<inter> S \<noteq> {}" "U - S \<noteq> {}"
proof -
have "U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}"
using assms by (simp add: frontier_of_closures)
then show "U \<inter> S \<noteq> {}"
using assms openin_Int_closure_of_eq_empty by fastforce
show "U - S \<noteq> {}"
proof -
have "\<exists>A. X closure_of (A - S) \<inter> U \<noteq> {}"
using \<open>U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}\<close> by blast
then have "\<not> U \<subseteq> S"
by (metis Diff_disjoint Diff_eq_empty_iff Int_Diff assms(1) inf_commute openin_Int_closure_of_eq_empty)
then show ?thesis
by blast
qed
qed
lemma frontier_of_subset_closedin: "closedin X S \<Longrightarrow> (X frontier_of S) \<subseteq> S"
using closure_of_eq frontier_of_def by fastforce
lemma frontier_of_empty [simp]: "X frontier_of {} = {}"
by (simp add: frontier_of_def)
lemma frontier_of_topspace [simp]: "X frontier_of topspace X = {}"
by (simp add: frontier_of_def)
lemma frontier_of_subset_eq:
assumes "S \<subseteq> topspace X"
shows "(X frontier_of S) \<subseteq> S \<longleftrightarrow> closedin X S"
proof
show "X frontier_of S \<subseteq> S \<Longrightarrow> closedin X S"
by (metis assms closure_of_subset_eq interior_of_subset interior_of_union_frontier_of le_sup_iff)
show "closedin X S \<Longrightarrow> X frontier_of S \<subseteq> S"
by (simp add: frontier_of_subset_closedin)
qed
lemma frontier_of_complement: "X frontier_of (topspace X - S) = X frontier_of S"
by (metis Diff_Diff_Int closure_of_restrict frontier_of_closures inf_commute)
lemma frontier_of_disjoint_eq:
assumes "S \<subseteq> topspace X"
shows "((X frontier_of S) \<inter> S = {} \<longleftrightarrow> openin X S)"
proof
assume "X frontier_of S \<inter> S = {}"
then have "closedin X (topspace X - S)"
using assms closure_of_subset frontier_of_def interior_of_eq interior_of_subset by fastforce
then show "openin X S"
using assms by (simp add: openin_closedin)
next
show "openin X S \<Longrightarrow> X frontier_of S \<inter> S = {}"
by (simp add: Diff_Diff_Int closedin_def frontier_of_openin inf.absorb_iff2 inf_commute)
qed
lemma frontier_of_disjoint_eq_alt:
"S \<subseteq> (topspace X - X frontier_of S) \<longleftrightarrow> openin X S"
proof (cases "S \<subseteq> topspace X")
case True
show ?thesis
using True frontier_of_disjoint_eq by auto
next
case False
then show ?thesis
by (meson Diff_subset openin_subset subset_trans)
qed
lemma frontier_of_Int:
"X frontier_of (S \<inter> T) =
X closure_of (S \<inter> T) \<inter> (X frontier_of S \<union> X frontier_of T)"
proof -
have *: "U \<subseteq> S \<and> U \<subseteq> T \<Longrightarrow> U \<inter> (S \<inter> A \<union> T \<inter> B) = U \<inter> (A \<union> B)" for U S T A B :: "'a set"
by blast
show ?thesis
by (simp add: frontier_of_closures closure_of_mono Diff_Int * flip: closure_of_Un)
qed
lemma frontier_of_Int_subset: "X frontier_of (S \<inter> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
by (simp add: frontier_of_Int)
lemma frontier_of_Int_closedin:
"\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> X frontier_of(S \<inter> T) = X frontier_of S \<inter> T \<union> S \<inter> X frontier_of T"
apply (simp add: frontier_of_Int closedin_Int closure_of_closedin)
using frontier_of_subset_closedin by blast
lemma frontier_of_Un_subset: "X frontier_of(S \<union> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
by (metis Diff_Un frontier_of_Int_subset frontier_of_complement)
lemma frontier_of_Union_subset:
"finite \<F> \<Longrightarrow> X frontier_of (\<Union>\<F>) \<subseteq> (\<Union>T \<in> \<F>. X frontier_of T)"
proof (induction \<F> rule: finite_induct)
case (insert A \<F>)
then show ?case
using frontier_of_Un_subset by fastforce
qed simp
lemma frontier_of_frontier_of_subset:
"X frontier_of (X frontier_of S) \<subseteq> X frontier_of S"
by (simp add: closedin_frontier_of frontier_of_subset_closedin)
lemma frontier_of_subtopology_open:
"openin X U \<Longrightarrow> (subtopology X U) frontier_of S = U \<inter> X frontier_of S"
by (simp add: Diff_Int_distrib closure_of_subtopology_open frontier_of_def interior_of_subtopology_open)
lemma discrete_topology_frontier_of [simp]:
"(discrete_topology U) frontier_of S = {}"
by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures)
subsection\<open>Continuous maps\<close>
definition continuous_map where
"continuous_map X Y f \<equiv>
(\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
(\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
lemma continuous_map:
"continuous_map X Y f \<longleftrightarrow>
f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
by (auto simp: continuous_map_def)
lemma continuous_map_image_subset_topspace:
"continuous_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
by (auto simp: continuous_map_def)
lemma continuous_map_on_empty: "topspace X = {} \<Longrightarrow> continuous_map X Y f"
by (auto simp: continuous_map_def)
lemma continuous_map_closedin:
"continuous_map X Y f \<longleftrightarrow>
(\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
(\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
proof -
have "(\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}) =
(\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
if "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
proof -
have eq: "{x \<in> topspace X. f x \<in> topspace Y \<and> f x \<notin> C} = (topspace X - {x \<in> topspace X. f x \<in> C})" for C
using that by blast
show ?thesis
proof (intro iffI allI impI)
fix C
assume "\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}" and "closedin Y C"
then have "openin X {x \<in> topspace X. f x \<in> topspace Y - C}" by blast
then show "closedin X {x \<in> topspace X. f x \<in> C}"
by (auto simp add: closedin_def eq)
next
fix U
assume "\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}" and "openin Y U"
then have "closedin X {x \<in> topspace X. f x \<in> topspace Y - U}" by blast
then show "openin X {x \<in> topspace X. f x \<in> U}"
by (auto simp add: openin_closedin_eq eq)
qed
qed
then show ?thesis
by (auto simp: continuous_map_def)
qed
lemma openin_continuous_map_preimage:
"\<lbrakk>continuous_map X Y f; openin Y U\<rbrakk> \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
by (simp add: continuous_map_def)
lemma closedin_continuous_map_preimage:
"\<lbrakk>continuous_map X Y f; closedin Y C\<rbrakk> \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}"
by (simp add: continuous_map_closedin)
lemma openin_continuous_map_preimage_gen:
assumes "continuous_map X Y f" "openin X U" "openin Y V"
shows "openin X {x \<in> U. f x \<in> V}"
proof -
have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
using assms(2) openin_closedin_eq by fastforce
show ?thesis
unfolding eq
using assms openin_continuous_map_preimage by fastforce
qed
lemma closedin_continuous_map_preimage_gen:
assumes "continuous_map X Y f" "closedin X U" "closedin Y V"
shows "closedin X {x \<in> U. f x \<in> V}"
proof -
have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
using assms(2) closedin_def by fastforce
show ?thesis
unfolding eq
using assms closedin_continuous_map_preimage by fastforce
qed
lemma continuous_map_image_closure_subset:
assumes "continuous_map X Y f"
shows "f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
proof -
have *: "f ` (topspace X) \<subseteq> topspace Y"
by (meson assms continuous_map)
have "X closure_of T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of (f ` T)}" if "T \<subseteq> topspace X" for T
proof (rule closure_of_minimal)
show "T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
using closure_of_subset * that by (fastforce simp: in_closure_of)
next
show "closedin X {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
using assms closedin_continuous_map_preimage_gen by fastforce
qed
then have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (f ` (topspace X \<inter> S))"
by blast
also have "\<dots> \<subseteq> Y closure_of (topspace Y \<inter> f ` S)"
using * by (blast intro!: closure_of_mono)
finally have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (topspace Y \<inter> f ` S)" .
then show ?thesis
by (metis closure_of_restrict)
qed
lemma continuous_map_subset_aux1: "continuous_map X Y f \<Longrightarrow>
(\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
using continuous_map_image_closure_subset by blast
lemma continuous_map_subset_aux2:
assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
shows "continuous_map X Y f"
unfolding continuous_map_closedin
proof (intro conjI ballI allI impI)
fix x
assume "x \<in> topspace X"
then show "f x \<in> topspace Y"
using assms closure_of_subset_topspace by fastforce
next
fix C
assume "closedin Y C"
then show "closedin X {x \<in> topspace X. f x \<in> C}"
proof (clarsimp simp flip: closure_of_subset_eq, intro conjI)
fix x
assume x: "x \<in> X closure_of {x \<in> topspace X. f x \<in> C}"
and "C \<subseteq> topspace Y" and "Y closure_of C \<subseteq> C"
show "x \<in> topspace X"
by (meson x in_closure_of)
have "{a \<in> topspace X. f a \<in> C} \<subseteq> topspace X"
by simp
moreover have "Y closure_of f ` {a \<in> topspace X. f a \<in> C} \<subseteq> C"
by (simp add: \<open>closedin Y C\<close> closure_of_minimal image_subset_iff)
ultimately have "f ` (X closure_of {a \<in> topspace X. f a \<in> C}) \<subseteq> C"
using assms by blast
then show "f x \<in> C"
using x by auto
qed
qed
lemma continuous_map_eq_image_closure_subset:
"continuous_map X Y f \<longleftrightarrow> (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
lemma continuous_map_eq_image_closure_subset_alt:
"continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
lemma continuous_map_eq_image_closure_subset_gen:
"continuous_map X Y f \<longleftrightarrow>
f ` (topspace X) \<subseteq> topspace Y \<and>
(\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
using continuous_map_subset_aux1 continuous_map_subset_aux2 continuous_map_image_subset_topspace by metis
lemma continuous_map_closure_preimage_subset:
"continuous_map X Y f
\<Longrightarrow> X closure_of {x \<in> topspace X. f x \<in> T}
\<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
unfolding continuous_map_closedin
by (rule closure_of_minimal) (use in_closure_of in \<open>fastforce+\<close>)
lemma continuous_map_frontier_frontier_preimage_subset:
assumes "continuous_map X Y f"
shows "X frontier_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y frontier_of T}"
proof -
have eq: "topspace X - {x \<in> topspace X. f x \<in> T} = {x \<in> topspace X. f x \<in> topspace Y - T}"
using assms unfolding continuous_map_def by blast
have "X closure_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
by (simp add: assms continuous_map_closure_preimage_subset)
moreover
have "X closure_of (topspace X - {x \<in> topspace X. f x \<in> T}) \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of (topspace Y - T)}"
using continuous_map_closure_preimage_subset [OF assms] eq by presburger
ultimately show ?thesis
by (auto simp: frontier_of_closures)
qed
lemma topology_finer_continuous_id:
"topspace X = topspace Y \<Longrightarrow> ((\<forall>S. openin X S \<longrightarrow> openin Y S) \<longleftrightarrow> continuous_map Y X id)"
unfolding continuous_map_def
apply auto
using openin_subopen openin_subset apply fastforce
using openin_subopen topspace_def by fastforce
lemma continuous_map_const [simp]:
"continuous_map X Y (\<lambda>x. C) \<longleftrightarrow> topspace X = {} \<or> C \<in> topspace Y"
proof (cases "topspace X = {}")
case False
show ?thesis
proof (cases "C \<in> topspace Y")
case True
with openin_subopen show ?thesis
by (auto simp: continuous_map_def)
next
case False
then show ?thesis
unfolding continuous_map_def by fastforce
qed
qed (auto simp: continuous_map_on_empty)
lemma continuous_map_compose:
assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
shows "continuous_map X X'' (g \<circ> f)"
unfolding continuous_map_def
proof (intro conjI ballI allI impI)
fix x
assume "x \<in> topspace X"
then show "(g \<circ> f) x \<in> topspace X''"
using assms unfolding continuous_map_def by force
next
fix U
assume "openin X'' U"
have eq: "{x \<in> topspace X. (g \<circ> f) x \<in> U} = {x \<in> topspace X. f x \<in> {y. y \<in> topspace X' \<and> g y \<in> U}}"
by auto (meson f continuous_map_def)
show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U}"
unfolding eq
using assms unfolding continuous_map_def
using \<open>openin X'' U\<close> by blast
qed
lemma continuous_map_eq:
assumes "continuous_map X X' f" and "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x" shows "continuous_map X X' g"
proof -
have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
using assms by auto
show ?thesis
using assms by (simp add: continuous_map_def eq)
qed
lemma restrict_continuous_map [simp]:
"topspace X \<subseteq> S \<Longrightarrow> continuous_map X X' (restrict f S) \<longleftrightarrow> continuous_map X X' f"
by (auto simp: elim!: continuous_map_eq)
lemma continuous_map_in_subtopology:
"continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f ` (topspace X) \<subseteq> S"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
show ?rhs
proof -
have "\<And>A. f ` (X closure_of A) \<subseteq> subtopology X' S closure_of f ` A"
by (meson L continuous_map_image_closure_subset)
then show ?thesis
by (metis (no_types) closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace continuous_map_eq_image_closure_subset dual_order.trans)
qed
next
assume R: ?rhs
then have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. f x \<in> U \<and> f x \<in> S}" for U
by auto
show ?lhs
using R
unfolding continuous_map
by (auto simp: topspace_subtopology openin_subtopology eq)
qed
lemma continuous_map_from_subtopology:
"continuous_map X X' f \<Longrightarrow> continuous_map (subtopology X S) X' f"
by (auto simp: continuous_map topspace_subtopology openin_subtopology)
lemma continuous_map_into_fulltopology:
"continuous_map X (subtopology X' T) f \<Longrightarrow> continuous_map X X' f"
by (auto simp: continuous_map_in_subtopology)
lemma continuous_map_into_subtopology:
"\<lbrakk>continuous_map X X' f; f ` topspace X \<subseteq> T\<rbrakk> \<Longrightarrow> continuous_map X (subtopology X' T) f"
by (auto simp: continuous_map_in_subtopology)
lemma continuous_map_from_subtopology_mono:
"\<lbrakk>continuous_map (subtopology X T) X' f; S \<subseteq> T\<rbrakk>
\<Longrightarrow> continuous_map (subtopology X S) X' f"
by (metis inf.absorb_iff2 continuous_map_from_subtopology subtopology_subtopology)
lemma continuous_map_from_discrete_topology [simp]:
"continuous_map (discrete_topology U) X f \<longleftrightarrow> f ` U \<subseteq> topspace X"
by (auto simp: continuous_map_def)
lemma continuous_map_iff_continuous_real [simp]: "continuous_map (subtopology euclideanreal S) euclideanreal g = continuous_on S g"
by (force simp: continuous_map openin_subtopology continuous_on_open_invariant)
lemma continuous_map_id [simp]: "continuous_map X X id"
unfolding continuous_map_def using openin_subopen topspace_def by fastforce
declare continuous_map_id [unfolded id_def, simp]
lemma continuous_map_id_subt [simp]: "continuous_map (subtopology X S) X id"
by (simp add: continuous_map_from_subtopology)
declare continuous_map_id_subt [unfolded id_def, simp]
subsection\<open>Open and closed maps (not a priori assumed continuous)\<close>
definition open_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
where "open_map X1 X2 f \<equiv> \<forall>U. openin X1 U \<longrightarrow> openin X2 (f ` U)"
definition closed_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
where "closed_map X1 X2 f \<equiv> \<forall>U. closedin X1 U \<longrightarrow> closedin X2 (f ` U)"
lemma open_map_imp_subset_topspace:
"open_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
unfolding open_map_def by (simp add: openin_subset)
lemma open_map_imp_subset:
"\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
by (meson order_trans open_map_imp_subset_topspace subset_image_iff)
lemma topology_finer_open_id:
"(\<forall>S. openin X S \<longrightarrow> openin X' S) \<longleftrightarrow> open_map X X' id"
unfolding open_map_def by auto
lemma open_map_id: "open_map X X id"
unfolding open_map_def by auto
lemma open_map_eq:
"\<lbrakk>open_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> open_map X X' g"
unfolding open_map_def
by (metis image_cong openin_subset subset_iff)
lemma open_map_inclusion_eq:
"open_map (subtopology X S) X id \<longleftrightarrow> openin X (topspace X \<inter> S)"
proof -
have *: "openin X (T \<inter> S)" if "openin X (S \<inter> topspace X)" "openin X T" for T
proof -
have "T \<subseteq> topspace X"
using that by (simp add: openin_subset)
with that show "openin X (T \<inter> S)"
by (metis inf.absorb1 inf.left_commute inf_commute openin_Int)
qed
show ?thesis
by (fastforce simp add: open_map_def Int_commute openin_subtopology_alt intro: *)
qed
lemma open_map_inclusion:
"openin X S \<Longrightarrow> open_map (subtopology X S) X id"
by (simp add: open_map_inclusion_eq openin_Int)
lemma open_map_compose:
"\<lbrakk>open_map X X' f; open_map X' X'' g\<rbrakk> \<Longrightarrow> open_map X X'' (g \<circ> f)"
by (metis (no_types, lifting) image_comp open_map_def)
lemma closed_map_imp_subset_topspace:
"closed_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
by (simp add: closed_map_def closedin_subset)
lemma closed_map_imp_subset:
"\<lbrakk>closed_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
using closed_map_imp_subset_topspace by blast
lemma topology_finer_closed_id:
"(\<forall>S. closedin X S \<longrightarrow> closedin X' S) \<longleftrightarrow> closed_map X X' id"
by (simp add: closed_map_def)
lemma closed_map_id: "closed_map X X id"
by (simp add: closed_map_def)
lemma closed_map_eq:
"\<lbrakk>closed_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> closed_map X X' g"
unfolding closed_map_def
by (metis image_cong closedin_subset subset_iff)
lemma closed_map_compose:
"\<lbrakk>closed_map X X' f; closed_map X' X'' g\<rbrakk> \<Longrightarrow> closed_map X X'' (g \<circ> f)"
by (metis (no_types, lifting) closed_map_def image_comp)
lemma closed_map_inclusion_eq:
"closed_map (subtopology X S) X id \<longleftrightarrow>
closedin X (topspace X \<inter> S)"
proof -
have *: "closedin X (T \<inter> S)" if "closedin X (S \<inter> topspace X)" "closedin X T" for T
proof -
have "T \<subseteq> topspace X"
using that by (simp add: closedin_subset)
with that show "closedin X (T \<inter> S)"
by (metis inf.absorb1 inf.left_commute inf_commute closedin_Int)
qed
show ?thesis
by (fastforce simp add: closed_map_def Int_commute closedin_subtopology_alt intro: *)
qed
lemma closed_map_inclusion: "closedin X S \<Longrightarrow> closed_map (subtopology X S) X id"
by (simp add: closed_map_inclusion_eq closedin_Int)
lemma open_map_into_subtopology:
"\<lbrakk>open_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> open_map X (subtopology X' S) f"
unfolding open_map_def openin_subtopology
using openin_subset by fastforce
lemma closed_map_into_subtopology:
"\<lbrakk>closed_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> closed_map X (subtopology X' S) f"
unfolding closed_map_def closedin_subtopology
using closedin_subset by fastforce
lemma open_map_into_discrete_topology:
"open_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
unfolding open_map_def openin_discrete_topology using openin_subset by blast
lemma closed_map_into_discrete_topology:
"closed_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
unfolding closed_map_def closedin_discrete_topology using closedin_subset by blast
lemma bijective_open_imp_closed_map:
"\<lbrakk>open_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> closed_map X X' f"
unfolding open_map_def closed_map_def closedin_def
by auto (metis Diff_subset inj_on_image_set_diff)
lemma bijective_closed_imp_open_map:
"\<lbrakk>closed_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> open_map X X' f"
unfolding closed_map_def open_map_def openin_closedin_eq
by auto (metis Diff_subset inj_on_image_set_diff)
lemma open_map_from_subtopology:
"\<lbrakk>open_map X X' f; openin X U\<rbrakk> \<Longrightarrow> open_map (subtopology X U) X' f"
unfolding open_map_def openin_subtopology_alt by blast
lemma closed_map_from_subtopology:
"\<lbrakk>closed_map X X' f; closedin X U\<rbrakk> \<Longrightarrow> closed_map (subtopology X U) X' f"
unfolding closed_map_def closedin_subtopology_alt by blast
lemma open_map_restriction:
"\<lbrakk>open_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
\<Longrightarrow> open_map (subtopology X U) (subtopology X' V) f"
unfolding open_map_def openin_subtopology_alt
apply clarify
apply (rename_tac T)
apply (rule_tac x="f ` T" in image_eqI)
using openin_closedin_eq by force+
lemma closed_map_restriction:
"\<lbrakk>closed_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
\<Longrightarrow> closed_map (subtopology X U) (subtopology X' V) f"
unfolding closed_map_def closedin_subtopology_alt
apply clarify
apply (rename_tac T)
apply (rule_tac x="f ` T" in image_eqI)
using closedin_def by force+
subsection\<open>Quotient maps\<close>
definition quotient_map where
"quotient_map X X' f \<longleftrightarrow>
f ` (topspace X) = topspace X' \<and>
(\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (openin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> openin X' U))"
lemma quotient_map_eq:
assumes "quotient_map X X' f" "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x"
shows "quotient_map X X' g"
proof -
have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
using assms by auto
show ?thesis
using assms
unfolding quotient_map_def
by (metis (mono_tags, lifting) eq image_cong)
qed
lemma quotient_map_compose:
assumes f: "quotient_map X X' f" and g: "quotient_map X' X'' g"
shows "quotient_map X X'' (g \<circ> f)"
unfolding quotient_map_def
proof (intro conjI allI impI)
show "(g \<circ> f) ` topspace X = topspace X''"
using assms by (simp only: image_comp [symmetric]) (simp add: quotient_map_def)
next
fix U''
assume "U'' \<subseteq> topspace X''"
define U' where "U' \<equiv> {y \<in> topspace X'. g y \<in> U''}"
have "U' \<subseteq> topspace X'"
by (auto simp add: U'_def)
then have U': "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
using assms unfolding quotient_map_def by simp
have eq: "{x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U''} = {x \<in> topspace X. (g \<circ> f) x \<in> U''}"
using f quotient_map_def by fastforce
have "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X {x \<in> topspace X. f x \<in> U'}"
using assms by (simp add: quotient_map_def U'_def eq)
also have "\<dots> = openin X'' U''"
using U'_def \<open>U'' \<subseteq> topspace X''\<close> U' g quotient_map_def by fastforce
finally show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X'' U''" .
qed
lemma quotient_map_from_composition:
assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g" and gf: "quotient_map X X'' (g \<circ> f)"
shows "quotient_map X' X'' g"
unfolding quotient_map_def
proof (intro conjI allI impI)
show "g ` topspace X' = topspace X''"
using assms unfolding continuous_map_def quotient_map_def by fastforce
next
fix U'' :: "'c set"
assume U'': "U'' \<subseteq> topspace X''"
have eq: "{x \<in> topspace X. g (f x) \<in> U''} = {x \<in> topspace X. f x \<in> {y. y \<in> topspace X' \<and> g y \<in> U''}}"
using continuous_map_def f by fastforce
show "openin X' {x \<in> topspace X'. g x \<in> U''} = openin X'' U''"
using assms unfolding continuous_map_def quotient_map_def
by (metis (mono_tags, lifting) Collect_cong U'' comp_apply eq)
qed
lemma quotient_imp_continuous_map:
"quotient_map X X' f \<Longrightarrow> continuous_map X X' f"
by (simp add: continuous_map openin_subset quotient_map_def)
lemma quotient_imp_surjective_map:
"quotient_map X X' f \<Longrightarrow> f ` (topspace X) = topspace X'"
by (simp add: quotient_map_def)
lemma quotient_map_closedin:
"quotient_map X X' f \<longleftrightarrow>
f ` (topspace X) = topspace X' \<and>
(\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (closedin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> closedin X' U))"
proof -
have eq: "(topspace X - {x \<in> topspace X. f x \<in> U'}) = {x \<in> topspace X. f x \<in> topspace X' \<and> f x \<notin> U'}"
if "f ` topspace X = topspace X'" "U' \<subseteq> topspace X'" for U'
using that by auto
have "(\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U) =
(\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U)"
if "f ` topspace X = topspace X'"
proof (rule iffI; intro allI impI subsetI)
fix U'
assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U"
and U': "U' \<subseteq> topspace X'"
show "closedin X {x \<in> topspace X. f x \<in> U'} = closedin X' U'"
using U' by (auto simp add: closedin_def simp flip: * [of "topspace X' - U'"] eq [OF that])
next
fix U' :: "'b set"
assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U"
and U': "U' \<subseteq> topspace X'"
show "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
using U' by (auto simp add: openin_closedin_eq simp flip: * [of "topspace X' - U'"] eq [OF that])
qed
then show ?thesis
unfolding quotient_map_def by force
qed
lemma continuous_open_imp_quotient_map:
assumes "continuous_map X X' f" and om: "open_map X X' f" and feq: "f ` (topspace X) = topspace X'"
shows "quotient_map X X' f"
proof -
{ fix U
assume U: "U \<subseteq> topspace X'" and "openin X {x \<in> topspace X. f x \<in> U}"
then have ope: "openin X' (f ` {x \<in> topspace X. f x \<in> U})"
using om unfolding open_map_def by blast
then have "openin X' U"
using U feq by (subst openin_subopen) force
}
moreover have "openin X {x \<in> topspace X. f x \<in> U}" if "U \<subseteq> topspace X'" and "openin X' U" for U
using that assms unfolding continuous_map_def by blast
ultimately show ?thesis
unfolding quotient_map_def using assms by blast
qed
lemma continuous_closed_imp_quotient_map:
assumes "continuous_map X X' f" and om: "closed_map X X' f" and feq: "f ` (topspace X) = topspace X'"
shows "quotient_map X X' f"
proof -
have "f ` {x \<in> topspace X. f x \<in> U} = U" if "U \<subseteq> topspace X'" for U
using that feq by auto
with assms show ?thesis
unfolding quotient_map_closedin closed_map_def continuous_map_closedin by auto
qed
lemma continuous_open_quotient_map:
"\<lbrakk>continuous_map X X' f; open_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
by (meson continuous_open_imp_quotient_map quotient_map_def)
lemma continuous_closed_quotient_map:
"\<lbrakk>continuous_map X X' f; closed_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
by (meson continuous_closed_imp_quotient_map quotient_map_def)
lemma injective_quotient_map:
assumes "inj_on f (topspace X)"
shows "quotient_map X X' f \<longleftrightarrow>
continuous_map X X' f \<and> open_map X X' f \<and> closed_map X X' f \<and> f ` (topspace X) = topspace X'"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
have "open_map X X' f"
proof (clarsimp simp add: open_map_def)
fix U
assume "openin X U"
then have "U \<subseteq> topspace X"
by (simp add: openin_subset)
moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
ultimately show "openin X' (f ` U)"
using L unfolding quotient_map_def
by (metis (no_types, lifting) Collect_cong \<open>openin X U\<close> image_mono)
qed
moreover have "closed_map X X' f"
proof (clarsimp simp add: closed_map_def)
fix U
assume "closedin X U"
then have "U \<subseteq> topspace X"
by (simp add: closedin_subset)
moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
ultimately show "closedin X' (f ` U)"
using L unfolding quotient_map_closedin
by (metis (no_types, lifting) Collect_cong \<open>closedin X U\<close> image_mono)
qed
ultimately show ?rhs
using L by (simp add: quotient_imp_continuous_map quotient_imp_surjective_map)
next
assume ?rhs
then show ?lhs
by (simp add: continuous_closed_imp_quotient_map)
qed
lemma continuous_compose_quotient_map:
assumes f: "quotient_map X X' f" and g: "continuous_map X X'' (g \<circ> f)"
shows "continuous_map X' X'' g"
unfolding quotient_map_def continuous_map_def
proof (intro conjI ballI allI impI)
show "\<And>x'. x' \<in> topspace X' \<Longrightarrow> g x' \<in> topspace X''"
using assms unfolding quotient_map_def
by (metis (no_types, hide_lams) continuous_map_image_subset_topspace image_comp image_subset_iff)
next
fix U'' :: "'c set"
assume U'': "openin X'' U''"
have "f ` topspace X = topspace X'"
by (simp add: f quotient_imp_surjective_map)
then have eq: "{x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U} = {x \<in> topspace X. g (f x) \<in> U}" for U
by auto
have "openin X {x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U''}"
unfolding eq using U'' g openin_continuous_map_preimage by fastforce
then have *: "openin X {x \<in> topspace X. f x \<in> {x \<in> topspace X'. g x \<in> U''}}"
by auto
show "openin X' {x \<in> topspace X'. g x \<in> U''}"
using f unfolding quotient_map_def
by (metis (no_types) Collect_subset *)
qed
lemma continuous_compose_quotient_map_eq:
"quotient_map X X' f \<Longrightarrow> continuous_map X X'' (g \<circ> f) \<longleftrightarrow> continuous_map X' X'' g"
using continuous_compose_quotient_map continuous_map_compose quotient_imp_continuous_map by blast
lemma quotient_map_compose_eq:
"quotient_map X X' f \<Longrightarrow> quotient_map X X'' (g \<circ> f) \<longleftrightarrow> quotient_map X' X'' g"
apply safe
apply (meson continuous_compose_quotient_map_eq quotient_imp_continuous_map quotient_map_from_composition)
by (simp add: quotient_map_compose)
lemma quotient_map_restriction:
assumes quo: "quotient_map X Y f" and U: "{x \<in> topspace X. f x \<in> V} = U" and disj: "openin Y V \<or> closedin Y V"
shows "quotient_map (subtopology X U) (subtopology Y V) f"
using disj
proof
assume V: "openin Y V"
with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
by (auto simp: openin_subset)
have fim: "f ` topspace X = topspace Y"
and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
using quo unfolding quotient_map_def by auto
have "openin X U"
using U V Y sub(2) by blast
show ?thesis
unfolding quotient_map_def
proof (intro conjI allI impI)
show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
using sub U fim by (auto simp: topspace_subtopology)
next
fix Y' :: "'b set"
assume "Y' \<subseteq> topspace (subtopology Y V)"
then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
by (simp_all add: topspace_subtopology)
then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
using U by blast
then show "openin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = openin (subtopology Y V) Y'"
using U V Y \<open>openin X U\<close> \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
by (simp add: topspace_subtopology openin_open_subtopology eq) (auto simp: openin_closedin_eq)
qed
next
assume V: "closedin Y V"
with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
by (auto simp: closedin_subset)
have fim: "f ` topspace X = topspace Y"
and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> U} = closedin Y U"
using quo unfolding quotient_map_closedin by auto
have "closedin X U"
using U V Y sub(2) by blast
show ?thesis
unfolding quotient_map_closedin
proof (intro conjI allI impI)
show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
using sub U fim by (auto simp: topspace_subtopology)
next
fix Y' :: "'b set"
assume "Y' \<subseteq> topspace (subtopology Y V)"
then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
by (simp_all add: topspace_subtopology)
then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
using U by blast
then show "closedin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = closedin (subtopology Y V) Y'"
using U V Y \<open>closedin X U\<close> \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
by (simp add: topspace_subtopology closedin_closed_subtopology eq) (auto simp: closedin_def)
qed
qed
lemma quotient_map_saturated_open:
"quotient_map X Y f \<longleftrightarrow>
continuous_map X Y f \<and> f ` (topspace X) = topspace Y \<and>
(\<forall>U. openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U \<longrightarrow> openin Y (f ` U))"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
then have fim: "f ` topspace X = topspace Y"
and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin Y U = openin X {x \<in> topspace X. f x \<in> U}"
unfolding quotient_map_def by auto
show ?rhs
proof (intro conjI allI impI)
show "continuous_map X Y f"
by (simp add: L quotient_imp_continuous_map)
show "f ` topspace X = topspace Y"
by (simp add: fim)
next
fix U :: "'a set"
assume U: "openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U"
then have sub: "f ` U \<subseteq> topspace Y" and eq: "{x \<in> topspace X. f x \<in> f ` U} = U"
using fim openin_subset by fastforce+
show "openin Y (f ` U)"
by (simp add: sub Y eq U)
qed
next
assume ?rhs
then have YX: "\<And>U. openin Y U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
and fim: "f ` topspace X = topspace Y"
and XY: "\<And>U. \<lbrakk>openin X U; {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U\<rbrakk> \<Longrightarrow> openin Y (f ` U)"
by (auto simp: quotient_map_def continuous_map_def)
show ?lhs
proof (simp add: quotient_map_def fim, intro allI impI iffI)
fix U :: "'b set"
assume "U \<subseteq> topspace Y" and X: "openin X {x \<in> topspace X. f x \<in> U}"
have feq: "f ` {x \<in> topspace X. f x \<in> U} = U"
using \<open>U \<subseteq> topspace Y\<close> fim by auto
show "openin Y U"
using XY [OF X] by (simp add: feq)
next
fix U :: "'b set"
assume "U \<subseteq> topspace Y" and Y: "openin Y U"
show "openin X {x \<in> topspace X. f x \<in> U}"
by (metis YX [OF Y])
qed
qed
subsection\<open> Separated Sets\<close>
definition separatedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
where "separatedin X S T \<equiv>
S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and>
S \<inter> X closure_of T = {} \<and> T \<inter> X closure_of S = {}"
lemma separatedin_empty [simp]:
"separatedin X S {} \<longleftrightarrow> S \<subseteq> topspace X"
"separatedin X {} S \<longleftrightarrow> S \<subseteq> topspace X"
by (simp_all add: separatedin_def)
lemma separatedin_refl [simp]:
"separatedin X S S \<longleftrightarrow> S = {}"
proof -
have "\<And>x. \<lbrakk>separatedin X S S; x \<in> S\<rbrakk> \<Longrightarrow> False"
by (metis all_not_in_conv closure_of_subset inf.orderE separatedin_def)
then show ?thesis
by auto
qed
lemma separatedin_sym:
"separatedin X S T \<longleftrightarrow> separatedin X T S"
by (auto simp: separatedin_def)
lemma separatedin_imp_disjoint:
"separatedin X S T \<Longrightarrow> disjnt S T"
by (meson closure_of_subset disjnt_def disjnt_subset2 separatedin_def)
lemma separatedin_mono:
"\<lbrakk>separatedin X S T; S' \<subseteq> S; T' \<subseteq> T\<rbrakk> \<Longrightarrow> separatedin X S' T'"
unfolding separatedin_def
using closure_of_mono by blast
lemma separatedin_open_sets:
"\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
unfolding disjnt_def separatedin_def
by (auto simp: openin_Int_closure_of_eq_empty openin_subset)
lemma separatedin_closed_sets:
"\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
by (metis closedin_def closure_of_eq disjnt_def inf_commute separatedin_def)
lemma separatedin_subtopology:
"separatedin (subtopology X U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> separatedin X S T"
apply (simp add: separatedin_def closure_of_subtopology topspace_subtopology)
apply (safe; metis Int_absorb1 inf.assoc inf.orderE insert_disjoint(2) mk_disjoint_insert)
done
lemma separatedin_discrete_topology:
"separatedin (discrete_topology U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> disjnt S T"
by (metis openin_discrete_topology separatedin_def separatedin_open_sets topspace_discrete_topology)
lemma separated_eq_distinguishable:
"separatedin X {x} {y} \<longleftrightarrow>
x \<in> topspace X \<and> y \<in> topspace X \<and>
(\<exists>U. openin X U \<and> x \<in> U \<and> (y \<notin> U)) \<and>
(\<exists>v. openin X v \<and> y \<in> v \<and> (x \<notin> v))"
by (force simp: separatedin_def closure_of_def)
lemma separatedin_Un [simp]:
"separatedin X S (T \<union> U) \<longleftrightarrow> separatedin X S T \<and> separatedin X S U"
"separatedin X (S \<union> T) U \<longleftrightarrow> separatedin X S U \<and> separatedin X T U"
by (auto simp: separatedin_def)
lemma separatedin_Union:
"finite \<F> \<Longrightarrow> separatedin X S (\<Union>\<F>) \<longleftrightarrow> S \<subseteq> topspace X \<and> (\<forall>T \<in> \<F>. separatedin X S T)"
"finite \<F> \<Longrightarrow> separatedin X (\<Union>\<F>) S \<longleftrightarrow> (\<forall>T \<in> \<F>. separatedin X S T) \<and> S \<subseteq> topspace X"
by (auto simp: separatedin_def closure_of_Union)
lemma separatedin_openin_diff:
"\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
unfolding separatedin_def
apply (intro conjI)
apply (meson Diff_subset openin_subset subset_trans)+
using openin_Int_closure_of_eq_empty by fastforce+
lemma separatedin_closedin_diff:
"\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
apply (simp add: separatedin_def Diff_Int_distrib2 closure_of_minimal inf_absorb2)
apply (meson Diff_subset closedin_subset subset_trans)
done
lemma separation_closedin_Un_gen:
"separatedin X S T \<longleftrightarrow>
S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
closedin (subtopology X (S \<union> T)) S \<and>
closedin (subtopology X (S \<union> T)) T"
apply (simp add: separatedin_def closedin_Int_closure_of disjnt_iff)
using closure_of_subset apply blast
done
lemma separation_openin_Un_gen:
"separatedin X S T \<longleftrightarrow>
S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and> disjnt S T \<and>
openin (subtopology X (S \<union> T)) S \<and>
openin (subtopology X (S \<union> T)) T"
unfolding openin_closedin_eq topspace_subtopology separation_closedin_Un_gen disjnt_def
by (auto simp: Diff_triv Int_commute Un_Diff inf_absorb1 topspace_def)
subsection\<open>Homeomorphisms\<close>
text\<open>(1-way and 2-way versions may be useful in places)\<close>
definition homeomorphic_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
where
"homeomorphic_map X Y f \<equiv> quotient_map X Y f \<and> inj_on f (topspace X)"
definition homeomorphic_maps :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> bool"
where
"homeomorphic_maps X Y f g \<equiv>
continuous_map X Y f \<and> continuous_map Y X g \<and>
(\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"
lemma homeomorphic_map_eq:
"\<lbrakk>homeomorphic_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> homeomorphic_map X Y g"
by (meson homeomorphic_map_def inj_on_cong quotient_map_eq)
lemma homeomorphic_maps_eq:
"\<lbrakk>homeomorphic_maps X Y f g;
\<And>x. x \<in> topspace X \<Longrightarrow> f x = f' x; \<And>y. y \<in> topspace Y \<Longrightarrow> g y = g' y\<rbrakk>
\<Longrightarrow> homeomorphic_maps X Y f' g'"
apply (simp add: homeomorphic_maps_def)
by (metis continuous_map_eq continuous_map_eq_image_closure_subset_gen image_subset_iff)
lemma homeomorphic_maps_sym:
"homeomorphic_maps X Y f g \<longleftrightarrow> homeomorphic_maps Y X g f"
by (auto simp: homeomorphic_maps_def)
lemma homeomorphic_maps_id:
"homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
then have "topspace X = topspace Y"
by (auto simp: homeomorphic_maps_def continuous_map_def)
with L show ?rhs
unfolding homeomorphic_maps_def
by (metis topology_finer_continuous_id topology_eq)
next
assume ?rhs
then show ?lhs
unfolding homeomorphic_maps_def by auto
qed
lemma homeomorphic_map_id [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
then have eq: "topspace X = topspace Y"
by (auto simp: homeomorphic_map_def continuous_map_def quotient_map_def)
then have "\<And>S. openin X S \<longrightarrow> openin Y S"
by (meson L homeomorphic_map_def injective_quotient_map topology_finer_open_id)
then show ?rhs
using L unfolding homeomorphic_map_def
by (metis eq quotient_imp_continuous_map topology_eq topology_finer_continuous_id)
next
assume ?rhs
then show ?lhs
unfolding homeomorphic_map_def
by (simp add: closed_map_id continuous_closed_imp_quotient_map)
qed
lemma homeomorphic_maps_i [simp]:"homeomorphic_maps X Y id id \<longleftrightarrow> Y = X"
by (metis (full_types) eq_id_iff homeomorphic_maps_id)
lemma homeomorphic_map_i [simp]: "homeomorphic_map X Y id \<longleftrightarrow> Y = X"
by (metis (no_types) eq_id_iff homeomorphic_map_id)
lemma homeomorphic_map_compose:
assumes "homeomorphic_map X Y f" "homeomorphic_map Y X'' g"
shows "homeomorphic_map X X'' (g \<circ> f)"
proof -
have "inj_on g (f ` topspace X)"
by (metis (no_types) assms homeomorphic_map_def quotient_imp_surjective_map)
then show ?thesis
using assms by (meson comp_inj_on homeomorphic_map_def quotient_map_compose_eq)
qed
lemma homeomorphic_maps_compose:
"homeomorphic_maps X Y f h \<and>
homeomorphic_maps Y X'' g k
\<Longrightarrow> homeomorphic_maps X X'' (g \<circ> f) (h \<circ> k)"
unfolding homeomorphic_maps_def
by (auto simp: continuous_map_compose; simp add: continuous_map_def)
lemma homeomorphic_eq_everything_map:
"homeomorphic_map X Y f \<longleftrightarrow>
continuous_map X Y f \<and> open_map X Y f \<and> closed_map X Y f \<and>
f ` (topspace X) = topspace Y \<and> inj_on f (topspace X)"
unfolding homeomorphic_map_def
by (force simp: injective_quotient_map intro: injective_quotient_map)
lemma homeomorphic_imp_continuous_map:
"homeomorphic_map X Y f \<Longrightarrow> continuous_map X Y f"
by (simp add: homeomorphic_eq_everything_map)
lemma homeomorphic_imp_open_map:
"homeomorphic_map X Y f \<Longrightarrow> open_map X Y f"
by (simp add: homeomorphic_eq_everything_map)
lemma homeomorphic_imp_closed_map:
"homeomorphic_map X Y f \<Longrightarrow> closed_map X Y f"
by (simp add: homeomorphic_eq_everything_map)
lemma homeomorphic_imp_surjective_map:
"homeomorphic_map X Y f \<Longrightarrow> f ` (topspace X) = topspace Y"
by (simp add: homeomorphic_eq_everything_map)
lemma homeomorphic_imp_injective_map:
"homeomorphic_map X Y f \<Longrightarrow> inj_on f (topspace X)"
by (simp add: homeomorphic_eq_everything_map)
lemma bijective_open_imp_homeomorphic_map:
"\<lbrakk>continuous_map X Y f; open_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
\<Longrightarrow> homeomorphic_map X Y f"
by (simp add: homeomorphic_map_def continuous_open_imp_quotient_map)
lemma bijective_closed_imp_homeomorphic_map:
"\<lbrakk>continuous_map X Y f; closed_map X Y f; f ` (topspace X) = topspace Y; inj_on f (topspace X)\<rbrakk>
\<Longrightarrow> homeomorphic_map X Y f"
by (simp add: continuous_closed_quotient_map homeomorphic_map_def)
lemma open_eq_continuous_inverse_map:
assumes X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> g(f x) = x"
and Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> g y \<in> topspace X \<and> f(g y) = y"
shows "open_map X Y f \<longleftrightarrow> continuous_map Y X g"
proof -
have eq: "{x \<in> topspace Y. g x \<in> U} = f ` U" if "openin X U" for U
using openin_subset [OF that] by (force simp: X Y image_iff)
show ?thesis
by (auto simp: Y open_map_def continuous_map_def eq)
qed
lemma closed_eq_continuous_inverse_map:
assumes X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> g(f x) = x"
and Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> g y \<in> topspace X \<and> f(g y) = y"
shows "closed_map X Y f \<longleftrightarrow> continuous_map Y X g"
proof -
have eq: "{x \<in> topspace Y. g x \<in> U} = f ` U" if "closedin X U" for U
using closedin_subset [OF that] by (force simp: X Y image_iff)
show ?thesis
by (auto simp: Y closed_map_def continuous_map_closedin eq)
qed
lemma homeomorphic_maps_map:
"homeomorphic_maps X Y f g \<longleftrightarrow>
homeomorphic_map X Y f \<and> homeomorphic_map Y X g \<and>
(\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> topspace Y. f(g y) = y)"
(is "?lhs = ?rhs")
proof
assume ?lhs
then have L: "continuous_map X Y f" "continuous_map Y X g" "\<forall>x\<in>topspace X. g (f x) = x" "\<forall>x'\<in>topspace Y. f (g x') = x'"
by (auto simp: homeomorphic_maps_def)
show ?rhs
proof (intro conjI bijective_open_imp_homeomorphic_map L)
show "open_map X Y f"
using L using open_eq_continuous_inverse_map [of concl: X Y f g] by (simp add: continuous_map_def)
show "open_map Y X g"
using L using open_eq_continuous_inverse_map [of concl: Y X g f] by (simp add: continuous_map_def)
show "f ` topspace X = topspace Y" "g ` topspace Y = topspace X"
using L by (force simp: continuous_map_closedin)+
show "inj_on f (topspace X)" "inj_on g (topspace Y)"
using L unfolding inj_on_def by metis+
qed
next
assume ?rhs
then show ?lhs
by (auto simp: homeomorphic_maps_def homeomorphic_imp_continuous_map)
qed
lemma homeomorphic_maps_imp_map:
"homeomorphic_maps X Y f g \<Longrightarrow> homeomorphic_map X Y f"
using homeomorphic_maps_map by blast
lemma homeomorphic_map_maps:
"homeomorphic_map X Y f \<longleftrightarrow> (\<exists>g. homeomorphic_maps X Y f g)"
(is "?lhs = ?rhs")
proof
assume ?lhs
then have L: "continuous_map X Y f" "open_map X Y f" "closed_map X Y f"
"f ` (topspace X) = topspace Y" "inj_on f (topspace X)"
by (auto simp: homeomorphic_eq_everything_map)
have X: "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y \<and> inv_into (topspace X) f (f x) = x"
using L by auto
have Y: "\<And>y. y \<in> topspace Y \<Longrightarrow> inv_into (topspace X) f y \<in> topspace X \<and> f (inv_into (topspace X) f y) = y"
by (simp add: L f_inv_into_f inv_into_into)
have "homeomorphic_maps X Y f (inv_into (topspace X) f)"
unfolding homeomorphic_maps_def
proof (intro conjI L)
show "continuous_map Y X (inv_into (topspace X) f)"
by (simp add: L X Y flip: open_eq_continuous_inverse_map [where f=f])
next
show "\<forall>x\<in>topspace X. inv_into (topspace X) f (f x) = x"
"\<forall>y\<in>topspace Y. f (inv_into (topspace X) f y) = y"
using X Y by auto
qed
then show ?rhs
by metis
next
assume ?rhs
then show ?lhs
using homeomorphic_maps_map by blast
qed
lemma homeomorphic_maps_involution:
"\<lbrakk>continuous_map X X f; \<And>x. x \<in> topspace X \<Longrightarrow> f(f x) = x\<rbrakk> \<Longrightarrow> homeomorphic_maps X X f f"
by (auto simp: homeomorphic_maps_def)
lemma homeomorphic_map_involution:
"\<lbrakk>continuous_map X X f; \<And>x. x \<in> topspace X \<Longrightarrow> f(f x) = x\<rbrakk> \<Longrightarrow> homeomorphic_map X X f"
using homeomorphic_maps_involution homeomorphic_maps_map by blast
lemma homeomorphic_map_openness:
assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
shows "openin Y (f ` U) \<longleftrightarrow> openin X U"
proof -
obtain g where "homeomorphic_maps X Y f g"
using assms by (auto simp: homeomorphic_map_maps)
then have g: "homeomorphic_map Y X g" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
by (auto simp: homeomorphic_maps_map)
then have "openin X U \<Longrightarrow> openin Y (f ` U)"
using hom homeomorphic_imp_open_map open_map_def by blast
show "openin Y (f ` U) = openin X U"
proof
assume L: "openin Y (f ` U)"
have "U = g ` (f ` U)"
using U gf by force
then show "openin X U"
by (metis L homeomorphic_imp_open_map open_map_def g)
next
assume "openin X U"
then show "openin Y (f ` U)"
using hom homeomorphic_imp_open_map open_map_def by blast
qed
qed
lemma homeomorphic_map_closedness:
assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
shows "closedin Y (f ` U) \<longleftrightarrow> closedin X U"
proof -
obtain g where "homeomorphic_maps X Y f g"
using assms by (auto simp: homeomorphic_map_maps)
then have g: "homeomorphic_map Y X g" and gf: "\<And>x. x \<in> topspace X \<Longrightarrow> g(f x) = x"
by (auto simp: homeomorphic_maps_map)
then have "closedin X U \<Longrightarrow> closedin Y (f ` U)"
using hom homeomorphic_imp_closed_map closed_map_def by blast
show "closedin Y (f ` U) = closedin X U"
proof
assume L: "closedin Y (f ` U)"
have "U = g ` (f ` U)"
using U gf by force
then show "closedin X U"
by (metis L homeomorphic_imp_closed_map closed_map_def g)
next
assume "closedin X U"
then show "closedin Y (f ` U)"
using hom homeomorphic_imp_closed_map closed_map_def by blast
qed
qed
lemma homeomorphic_map_openness_eq:
"homeomorphic_map X Y f \<Longrightarrow> openin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> openin Y (f ` U)"
by (meson homeomorphic_map_openness openin_closedin_eq)
lemma homeomorphic_map_closedness_eq:
"homeomorphic_map X Y f \<Longrightarrow> closedin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> closedin Y (f ` U)"
by (meson closedin_subset homeomorphic_map_closedness)
lemma all_openin_homeomorphic_image:
assumes "homeomorphic_map X Y f"
shows "(\<forall>V. openin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> P(f ` U))" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (meson assms homeomorphic_map_openness_eq)
next
assume ?rhs
then show ?lhs
by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_openness openin_subset subset_image_iff)
qed
lemma all_closedin_homeomorphic_image:
assumes "homeomorphic_map X Y f"
shows "(\<forall>V. closedin Y V \<longrightarrow> P V) \<longleftrightarrow> (\<forall>U. closedin X U \<longrightarrow> P(f ` U))" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (meson assms homeomorphic_map_closedness_eq)
next
assume ?rhs
then show ?lhs
by (metis (no_types, lifting) assms homeomorphic_imp_surjective_map homeomorphic_map_closedness closedin_subset subset_image_iff)
qed
lemma homeomorphic_map_derived_set_of:
assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
shows "Y derived_set_of (f ` S) = f ` (X derived_set_of S)"
proof -
have fim: "f ` (topspace X) = topspace Y" and inj: "inj_on f (topspace X)"
using hom by (auto simp: homeomorphic_eq_everything_map)
have iff: "(\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T)) =
(\<forall>T. T \<subseteq> topspace Y \<longrightarrow> f x \<in> T \<longrightarrow> openin Y T \<longrightarrow> (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> T))"
if "x \<in> topspace X" for x
proof -
have 1: "(x \<in> T \<and> openin X T) = (T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T))" for T
by (meson hom homeomorphic_map_openness_eq inj inj_on_image_mem_iff that)
have 2: "(\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T) = (\<exists>y. y \<noteq> f x \<and> y \<in> f ` S \<and> y \<in> f ` T)" (is "?lhs = ?rhs")
if "T \<subseteq> topspace X \<and> f x \<in> f ` T \<and> openin Y (f ` T)" for T
proof
show "?lhs \<Longrightarrow> ?rhs"
by (meson "1" imageI inj inj_on_eq_iff inj_on_subset that)
show "?rhs \<Longrightarrow> ?lhs"
using S inj inj_onD that by fastforce
qed
show ?thesis
apply (simp flip: fim add: all_subset_image)
apply (simp flip: imp_conjL)
by (intro all_cong1 imp_cong 1 2)
qed
have *: "\<lbrakk>T = f ` S; \<And>x. x \<in> S \<Longrightarrow> P x \<longleftrightarrow> Q(f x)\<rbrakk> \<Longrightarrow> {y. y \<in> T \<and> Q y} = f ` {x \<in> S. P x}" for T S P Q
by auto
show ?thesis
unfolding derived_set_of_def
apply (rule *)
using fim apply blast
using iff openin_subset by force
qed
lemma homeomorphic_map_closure_of:
assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
shows "Y closure_of (f ` S) = f ` (X closure_of S)"
unfolding closure_of
using homeomorphic_imp_surjective_map [OF hom] S
by (auto simp: in_derived_set_of homeomorphic_map_derived_set_of [OF assms])
lemma homeomorphic_map_interior_of:
assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
shows "Y interior_of (f ` S) = f ` (X interior_of S)"
proof -
{ fix y
assume "y \<in> topspace Y" and "y \<notin> Y closure_of (topspace Y - f ` S)"
then have "y \<in> f ` (topspace X - X closure_of (topspace X - S))"
using homeomorphic_eq_everything_map [THEN iffD1, OF hom] homeomorphic_map_closure_of [OF hom]
by (metis DiffI Diff_subset S closure_of_subset_topspace inj_on_image_set_diff) }
moreover
{ fix x
assume "x \<in> topspace X"
then have "f x \<in> topspace Y"
using hom homeomorphic_imp_surjective_map by blast }
moreover
{ fix x
assume "x \<in> topspace X" and "x \<notin> X closure_of (topspace X - S)" and "f x \<in> Y closure_of (topspace Y - f ` S)"
then have "False"
using homeomorphic_map_closure_of [OF hom] hom
unfolding homeomorphic_eq_everything_map
by (metis (no_types, lifting) Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff_alt inj_on_image_set_diff) }
ultimately show ?thesis
by (auto simp: interior_of_closure_of)
qed
lemma homeomorphic_map_frontier_of:
assumes hom: "homeomorphic_map X Y f" and S: "S \<subseteq> topspace X"
shows "Y frontier_of (f ` S) = f ` (X frontier_of S)"
unfolding frontier_of_def
proof (intro equalityI subsetI DiffI)
fix y
assume "y \<in> Y closure_of f ` S - Y interior_of f ` S"
then show "y \<in> f ` (X closure_of S - X interior_of S)"
using S hom homeomorphic_map_closure_of homeomorphic_map_interior_of by fastforce
next
fix y
assume "y \<in> f ` (X closure_of S - X interior_of S)"
then show "y \<in> Y closure_of f ` S"
using S hom homeomorphic_map_closure_of by fastforce
next
fix x
assume "x \<in> f ` (X closure_of S - X interior_of S)"
then obtain y where y: "x = f y" "y \<in> X closure_of S" "y \<notin> X interior_of S"
by blast
then have "y \<in> topspace X"
by (simp add: in_closure_of)
then have "f y \<notin> f ` (X interior_of S)"
by (meson hom homeomorphic_eq_everything_map inj_on_image_mem_iff_alt interior_of_subset_topspace y(3))
then show "x \<notin> Y interior_of f ` S"
using S hom homeomorphic_map_interior_of y(1) by blast
qed
lemma homeomorphic_maps_subtopologies:
"\<lbrakk>homeomorphic_maps X Y f g; f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
\<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
unfolding homeomorphic_maps_def
by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)
lemma homeomorphic_maps_subtopologies_alt:
"\<lbrakk>homeomorphic_maps X Y f g; f ` (topspace X \<inter> S) \<subseteq> T; g ` (topspace Y \<inter> T) \<subseteq> S\<rbrakk>
\<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
unfolding homeomorphic_maps_def
by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)
lemma homeomorphic_map_subtopologies:
"\<lbrakk>homeomorphic_map X Y f; f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
\<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
by (meson homeomorphic_map_maps homeomorphic_maps_subtopologies)
lemma homeomorphic_map_subtopologies_alt:
"\<lbrakk>homeomorphic_map X Y f;
\<And>x. \<lbrakk>x \<in> topspace X; f x \<in> topspace Y\<rbrakk> \<Longrightarrow> f x \<in> T \<longleftrightarrow> x \<in> S\<rbrakk>
\<Longrightarrow> homeomorphic_map (subtopology X S) (subtopology Y T) f"
unfolding homeomorphic_map_maps
apply (erule ex_forward)
apply (rule homeomorphic_maps_subtopologies)
apply (auto simp: homeomorphic_maps_def continuous_map_def)
by (metis IntI image_iff)
subsection\<open>Relation of homeomorphism between topological spaces\<close>
definition homeomorphic_space (infixr "homeomorphic'_space" 50)
where "X homeomorphic_space Y \<equiv> \<exists>f g. homeomorphic_maps X Y f g"
lemma homeomorphic_space_refl: "X homeomorphic_space X"
by (meson homeomorphic_maps_id homeomorphic_space_def)
lemma homeomorphic_space_sym:
"X homeomorphic_space Y \<longleftrightarrow> Y homeomorphic_space X"
unfolding homeomorphic_space_def by (metis homeomorphic_maps_sym)
lemma homeomorphic_space_trans:
"\<lbrakk>X1 homeomorphic_space X2; X2 homeomorphic_space X3\<rbrakk> \<Longrightarrow> X1 homeomorphic_space X3"
unfolding homeomorphic_space_def by (metis homeomorphic_maps_compose)
lemma homeomorphic_space:
"X homeomorphic_space Y \<longleftrightarrow> (\<exists>f. homeomorphic_map X Y f)"
by (simp add: homeomorphic_map_maps homeomorphic_space_def)
lemma homeomorphic_maps_imp_homeomorphic_space:
"homeomorphic_maps X Y f g \<Longrightarrow> X homeomorphic_space Y"
unfolding homeomorphic_space_def by metis
lemma homeomorphic_map_imp_homeomorphic_space:
"homeomorphic_map X Y f \<Longrightarrow> X homeomorphic_space Y"
unfolding homeomorphic_map_maps
using homeomorphic_space_def by blast
lemma homeomorphic_empty_space:
"X homeomorphic_space Y \<Longrightarrow> topspace X = {} \<longleftrightarrow> topspace Y = {}"
by (metis homeomorphic_imp_surjective_map homeomorphic_space image_is_empty)
lemma homeomorphic_empty_space_eq:
assumes "topspace X = {}"
shows "X homeomorphic_space Y \<longleftrightarrow> topspace Y = {}"
proof -
have "\<forall>f t. continuous_map X (t::'b topology) f"
using assms continuous_map_on_empty by blast
then show ?thesis
by (metis (no_types) assms continuous_map_on_empty empty_iff homeomorphic_empty_space homeomorphic_maps_def homeomorphic_space_def)
qed
subsection\<open>Connected topological spaces\<close>
definition connected_space :: "'a topology \<Rightarrow> bool" where
"connected_space X \<equiv>
\<not>(\<exists>E1 E2. openin X E1 \<and> openin X E2 \<and>
topspace X \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
definition connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
"connectedin X S \<equiv> S \<subseteq> topspace X \<and> connected_space (subtopology X S)"
lemma connectedin_subset_topspace: "connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
by (simp add: connectedin_def)
lemma connectedin_topspace:
"connectedin X (topspace X) \<longleftrightarrow> connected_space X"
by (simp add: connectedin_def)
lemma connected_space_subtopology:
"connectedin X S \<Longrightarrow> connected_space (subtopology X S)"
by (simp add: connectedin_def)
lemma connectedin_subtopology:
"connectedin (subtopology X S) T \<longleftrightarrow> connectedin X T \<and> T \<subseteq> S"
by (force simp: connectedin_def subtopology_subtopology topspace_subtopology inf_absorb2)
lemma connected_space_eq:
"connected_space X \<longleftrightarrow>
(\<nexists>E1 E2. openin X E1 \<and> openin X E2 \<and> E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
unfolding connected_space_def
by (metis openin_Un openin_subset subset_antisym)
lemma connected_space_closedin:
"connected_space X \<longleftrightarrow>
(\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and> topspace X \<subseteq> E1 \<union> E2 \<and>
E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})" (is "?lhs = ?rhs")
proof
assume ?lhs
then have L: "\<And>E1 E2. \<lbrakk>openin X E1; E1 \<inter> E2 = {}; topspace X \<subseteq> E1 \<union> E2; openin X E2\<rbrakk> \<Longrightarrow> E1 = {} \<or> E2 = {}"
by (simp add: connected_space_def)
show ?rhs
unfolding connected_space_def
proof clarify
fix E1 E2
assume "closedin X E1" and "closedin X E2" and "topspace X \<subseteq> E1 \<union> E2" and "E1 \<inter> E2 = {}"
and "E1 \<noteq> {}" and "E2 \<noteq> {}"
have "E1 \<union> E2 = topspace X"
by (meson Un_subset_iff \<open>closedin X E1\<close> \<open>closedin X E2\<close> \<open>topspace X \<subseteq> E1 \<union> E2\<close> closedin_def subset_antisym)
then have "topspace X - E2 = E1"
using \<open>E1 \<inter> E2 = {}\<close> by fastforce
then have "topspace X = E1"
using \<open>E1 \<noteq> {}\<close> L \<open>closedin X E1\<close> \<open>closedin X E2\<close> by blast
then show "False"
using \<open>E1 \<inter> E2 = {}\<close> \<open>E1 \<union> E2 = topspace X\<close> \<open>E2 \<noteq> {}\<close> by blast
qed
next
assume R: ?rhs
show ?lhs
unfolding connected_space_def
proof clarify
fix E1 E2
assume "openin X E1" and "openin X E2" and "topspace X \<subseteq> E1 \<union> E2" and "E1 \<inter> E2 = {}"
and "E1 \<noteq> {}" and "E2 \<noteq> {}"
have "E1 \<union> E2 = topspace X"
by (meson Un_subset_iff \<open>openin X E1\<close> \<open>openin X E2\<close> \<open>topspace X \<subseteq> E1 \<union> E2\<close> openin_closedin_eq subset_antisym)
then have "topspace X - E2 = E1"
using \<open>E1 \<inter> E2 = {}\<close> by fastforce
then have "topspace X = E1"
using \<open>E1 \<noteq> {}\<close> R \<open>openin X E1\<close> \<open>openin X E2\<close> by blast
then show "False"
using \<open>E1 \<inter> E2 = {}\<close> \<open>E1 \<union> E2 = topspace X\<close> \<open>E2 \<noteq> {}\<close> by blast
qed
qed
lemma connected_space_closedin_eq:
"connected_space X \<longleftrightarrow>
(\<nexists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
apply (simp add: connected_space_closedin)
apply (intro all_cong)
using closedin_subset apply blast
done
lemma connected_space_clopen_in:
"connected_space X \<longleftrightarrow>
(\<forall>T. openin X T \<and> closedin X T \<longrightarrow> T = {} \<or> T = topspace X)"
proof -
have eq: "openin X E1 \<and> openin X E2 \<and> E1 \<union> E2 = topspace X \<and> E1 \<inter> E2 = {} \<and> P
\<longleftrightarrow> E2 = topspace X - E1 \<and> openin X E1 \<and> openin X E2 \<and> P" for E1 E2 P
using openin_subset by blast
show ?thesis
unfolding connected_space_eq eq closedin_def
by (auto simp: openin_closedin_eq)
qed
lemma connectedin:
"connectedin X S \<longleftrightarrow>
S \<subseteq> topspace X \<and>
(\<nexists>E1 E2.
openin X E1 \<and> openin X E2 \<and>
S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 \<inter> S = {} \<and> E1 \<inter> S \<noteq> {} \<and> E2 \<inter> S \<noteq> {})"
proof -
have *: "(\<exists>E1:: 'a set. \<exists>E2:: 'a set. (\<exists>T1:: 'a set. P1 T1 \<and> E1 = f1 T1) \<and> (\<exists>T2:: 'a set. P2 T2 \<and> E2 = f2 T2) \<and>
R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
by auto
show ?thesis
unfolding connectedin_def connected_space_def openin_subtopology topspace_subtopology Not_eq_iff *
apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
apply (blast elim: dest!: openin_subset)+
done
qed
lemma connectedin_iff_connected_real [simp]:
"connectedin euclideanreal S \<longleftrightarrow> connected S"
by (simp add: connected_def connectedin)
lemma connectedin_closedin:
"connectedin X S \<longleftrightarrow>
S \<subseteq> topspace X \<and>
\<not>(\<exists>E1 E2. closedin X E1 \<and> closedin X E2 \<and>
S \<subseteq> (E1 \<union> E2) \<and>
(E1 \<inter> E2 \<inter> S = {}) \<and>
\<not>(E1 \<inter> S = {}) \<and> \<not>(E2 \<inter> S = {}))"
proof -
have *: "(\<exists>E1:: 'a set. \<exists>E2:: 'a set. (\<exists>T1:: 'a set. P1 T1 \<and> E1 = f1 T1) \<and> (\<exists>T2:: 'a set. P2 T2 \<and> E2 = f2 T2) \<and>
R E1 E2) \<longleftrightarrow> (\<exists>T1 T2. P1 T1 \<and> P2 T2 \<and> R(f1 T1) (f2 T2))" for P1 f1 P2 f2 R
by auto
show ?thesis
unfolding connectedin_def connected_space_closedin closedin_subtopology topspace_subtopology Not_eq_iff *
apply (intro conj_cong arg_cong [where f=Not] ex_cong1 refl)
apply (blast elim: dest!: openin_subset)+
done
qed
lemma connectedin_empty [simp]: "connectedin X {}"
by (simp add: connectedin)
lemma connected_space_topspace_empty:
"topspace X = {} \<Longrightarrow> connected_space X"
using connectedin_topspace by fastforce
lemma connectedin_sing [simp]: "connectedin X {a} \<longleftrightarrow> a \<in> topspace X"
by (simp add: connectedin)
lemma connectedin_absolute [simp]:
"connectedin (subtopology X S) S \<longleftrightarrow> connectedin X S"
apply (simp only: connectedin_def topspace_subtopology subtopology_subtopology)
apply (intro conj_cong imp_cong arg_cong [where f=Not] all_cong1 ex_cong1 refl)
by auto
lemma connectedin_Union:
assumes \<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> connectedin X S" and ne: "\<Inter>\<U> \<noteq> {}"
shows "connectedin X (\<Union>\<U>)"
proof -
have "\<Union>\<U> \<subseteq> topspace X"
using \<U> by (simp add: Union_least connectedin_def)
moreover have False
if "openin X E1" "openin X E2" and cover: "\<Union>\<U> \<subseteq> E1 \<union> E2" and disj: "E1 \<inter> E2 \<inter> \<Union>\<U> = {}"
and overlap1: "E1 \<inter> \<Union>\<U> \<noteq> {}" and overlap2: "E2 \<inter> \<Union>\<U> \<noteq> {}"
for E1 E2
proof -
have disjS: "E1 \<inter> E2 \<inter> S = {}" if "S \<in> \<U>" for S
using Diff_triv that disj by auto
have coverS: "S \<subseteq> E1 \<union> E2" if "S \<in> \<U>" for S
using that cover by blast
have "\<U> \<noteq> {}"
using overlap1 by blast
obtain a where a: "\<And>U. U \<in> \<U> \<Longrightarrow> a \<in> U"
using ne by force
with \<open>\<U> \<noteq> {}\<close> have "a \<in> \<Union>\<U>"
by blast
then consider "a \<in> E1" | "a \<in> E2"
using \<open>\<Union>\<U> \<subseteq> E1 \<union> E2\<close> by auto
then show False
proof cases
case 1
then obtain b S where "b \<in> E2" "b \<in> S" "S \<in> \<U>"
using overlap2 by blast
then show ?thesis
using "1" \<open>openin X E1\<close> \<open>openin X E2\<close> disjS coverS a [OF \<open>S \<in> \<U>\<close>] \<U>[OF \<open>S \<in> \<U>\<close>]
unfolding connectedin
by (meson disjoint_iff_not_equal)
next
case 2
then obtain b S where "b \<in> E1" "b \<in> S" "S \<in> \<U>"
using overlap1 by blast
then show ?thesis
using "2" \<open>openin X E1\<close> \<open>openin X E2\<close> disjS coverS a [OF \<open>S \<in> \<U>\<close>] \<U>[OF \<open>S \<in> \<U>\<close>]
unfolding connectedin
by (meson disjoint_iff_not_equal)
qed
qed
ultimately show ?thesis
unfolding connectedin by blast
qed
lemma connectedin_Un:
"\<lbrakk>connectedin X S; connectedin X T; S \<inter> T \<noteq> {}\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
using connectedin_Union [of "{S,T}"] by auto
lemma connected_space_subconnected:
"connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. \<exists>S. connectedin X S \<and> x \<in> S \<and> y \<in> S)" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
using connectedin_topspace by blast
next
assume R [rule_format]: ?rhs
have False if "openin X U" "openin X V" and disj: "U \<inter> V = {}" and cover: "topspace X \<subseteq> U \<union> V"
and "U \<noteq> {}" "V \<noteq> {}" for U V
proof -
obtain u v where "u \<in> U" "v \<in> V"
using \<open>U \<noteq> {}\<close> \<open>V \<noteq> {}\<close> by auto
then obtain T where "u \<in> T" "v \<in> T" and T: "connectedin X T"
using R [of u v] that
by (meson \<open>openin X U\<close> \<open>openin X V\<close> subsetD openin_subset)
then show False
using that unfolding connectedin
by (metis IntI \<open>u \<in> U\<close> \<open>v \<in> V\<close> empty_iff inf_bot_left subset_trans)
qed
then show ?lhs
by (auto simp: connected_space_def)
qed
lemma connectedin_intermediate_closure_of:
assumes "connectedin X S" "S \<subseteq> T" "T \<subseteq> X closure_of S"
shows "connectedin X T"
proof -
have S: "S \<subseteq> topspace X"and T: "T \<subseteq> topspace X"
using assms by (meson closure_of_subset_topspace dual_order.trans)+
show ?thesis
using assms
apply (simp add: connectedin closure_of_subset_topspace S T)
apply (elim all_forward imp_forward2 asm_rl)
apply (blast dest: openin_Int_closure_of_eq_empty [of X _ S])+
done
qed
lemma connectedin_closure_of:
"connectedin X S \<Longrightarrow> connectedin X (X closure_of S)"
by (meson closure_of_subset connectedin_def connectedin_intermediate_closure_of subset_refl)
lemma connectedin_separation:
"connectedin X S \<longleftrightarrow>
S \<subseteq> topspace X \<and>
(\<nexists>C1 C2. C1 \<union> C2 = S \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> C1 \<inter> X closure_of C2 = {} \<and> C2 \<inter> X closure_of C1 = {})" (is "?lhs = ?rhs")
unfolding connectedin_def connected_space_closedin_eq closedin_Int_closure_of topspace_subtopology
apply (intro conj_cong refl arg_cong [where f=Not])
apply (intro ex_cong1 iffI, blast)
using closure_of_subset_Int by force
lemma connectedin_eq_not_separated:
"connectedin X S \<longleftrightarrow>
S \<subseteq> topspace X \<and>
(\<nexists>C1 C2. C1 \<union> C2 = S \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
apply (simp add: separatedin_def connectedin_separation)
apply (intro conj_cong all_cong1 refl, blast)
done
lemma connectedin_eq_not_separated_subset:
"connectedin X S \<longleftrightarrow>
S \<subseteq> topspace X \<and> (\<nexists>C1 C2. S \<subseteq> C1 \<union> C2 \<and> S \<inter> C1 \<noteq> {} \<and> S \<inter> C2 \<noteq> {} \<and> separatedin X C1 C2)"
proof -
have *: "\<forall>C1 C2. S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
if "\<And>C1 C2. C1 \<union> C2 = S \<longrightarrow> C1 = {} \<or> C2 = {} \<or> \<not> separatedin X C1 C2"
proof (intro allI)
fix C1 C2
show "S \<subseteq> C1 \<union> C2 \<longrightarrow> S \<inter> C1 = {} \<or> S \<inter> C2 = {} \<or> \<not> separatedin X C1 C2"
using that [of "S \<inter> C1" "S \<inter> C2"]
by (auto simp: separatedin_mono)
qed
show ?thesis
apply (simp add: connectedin_eq_not_separated)
apply (intro conj_cong refl iffI *)
apply (blast elim!: all_forward)+
done
qed
lemma connected_space_eq_not_separated:
"connected_space X \<longleftrightarrow>
(\<nexists>C1 C2. C1 \<union> C2 = topspace X \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
by (simp add: connectedin_eq_not_separated flip: connectedin_topspace)
lemma connected_space_eq_not_separated_subset:
"connected_space X \<longleftrightarrow>
(\<nexists>C1 C2. topspace X \<subseteq> C1 \<union> C2 \<and> C1 \<noteq> {} \<and> C2 \<noteq> {} \<and> separatedin X C1 C2)"
apply (simp add: connected_space_eq_not_separated)
apply (intro all_cong1)
by (metis Un_absorb dual_order.antisym separatedin_def subset_refl sup_mono)
lemma connectedin_subset_separated_union:
"\<lbrakk>connectedin X C; separatedin X S T; C \<subseteq> S \<union> T\<rbrakk> \<Longrightarrow> C \<subseteq> S \<or> C \<subseteq> T"
unfolding connectedin_eq_not_separated_subset by blast
lemma connectedin_nonseparated_union:
"\<lbrakk>connectedin X S; connectedin X T; \<not>separatedin X S T\<rbrakk> \<Longrightarrow> connectedin X (S \<union> T)"
apply (simp add: connectedin_eq_not_separated_subset, auto)
apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono sup_commute)
apply (metis (no_types, hide_lams) Diff_subset_conv Diff_triv disjoint_iff_not_equal separatedin_mono separatedin_sym sup_commute)
by (meson disjoint_iff_not_equal)
lemma connected_space_closures:
"connected_space X \<longleftrightarrow>
(\<nexists>e1 e2. e1 \<union> e2 = topspace X \<and> X closure_of e1 \<inter> X closure_of e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
unfolding connected_space_closedin_eq
by (metis Un_upper1 Un_upper2 closedin_closure_of closure_of_Un closure_of_eq_empty closure_of_topspace)
next
assume ?rhs
then show ?lhs
unfolding connected_space_closedin_eq
by (metis closure_of_eq)
qed
lemma connectedin_inter_frontier_of:
assumes "connectedin X S" "S \<inter> T \<noteq> {}" "S - T \<noteq> {}"
shows "S \<inter> X frontier_of T \<noteq> {}"
proof -
have "S \<subseteq> topspace X" and *:
"\<And>E1 E2. openin X E1 \<longrightarrow> openin X E2 \<longrightarrow> E1 \<inter> E2 \<inter> S = {} \<longrightarrow> S \<subseteq> E1 \<union> E2 \<longrightarrow> E1 \<inter> S = {} \<or> E2 \<inter> S = {}"
using \<open>connectedin X S\<close> by (auto simp: connectedin)
have "S - (topspace X \<inter> T) \<noteq> {}"
using assms(3) by blast
moreover
have "S \<inter> topspace X \<inter> T \<noteq> {}"
using assms(1) assms(2) connectedin by fastforce
moreover
have False if "S \<inter> T \<noteq> {}" "S - T \<noteq> {}" "T \<subseteq> topspace X" "S \<inter> X frontier_of T = {}" for T
proof -
have null: "S \<inter> (X closure_of T - X interior_of T) = {}"
using that unfolding frontier_of_def by blast
have 1: "X interior_of T \<inter> (topspace X - X closure_of T) \<inter> S = {}"
by (metis Diff_disjoint inf_bot_left interior_of_Int interior_of_complement interior_of_empty)
have 2: "S \<subseteq> X interior_of T \<union> (topspace X - X closure_of T)"
using that \<open>S \<subseteq> topspace X\<close> null by auto
have 3: "S \<inter> X interior_of T \<noteq> {}"
using closure_of_subset that(1) that(3) null by fastforce
show ?thesis
using null \<open>S \<subseteq> topspace X\<close> that * [of "X interior_of T" "topspace X - X closure_of T"]
apply (clarsimp simp add: openin_diff 1 2)
apply (simp add: Int_commute Diff_Int_distrib 3)
by (metis Int_absorb2 contra_subsetD interior_of_subset)
qed
ultimately show ?thesis
by (metis Int_lower1 frontier_of_restrict inf_assoc)
qed
lemma connectedin_continuous_map_image:
assumes f: "continuous_map X Y f" and "connectedin X S"
shows "connectedin Y (f ` S)"
proof -
have "S \<subseteq> topspace X" and *:
"\<And>E1 E2. openin X E1 \<longrightarrow> openin X E2 \<longrightarrow> E1 \<inter> E2 \<inter> S = {} \<longrightarrow> S \<subseteq> E1 \<union> E2 \<longrightarrow> E1 \<inter> S = {} \<or> E2 \<inter> S = {}"
using \<open>connectedin X S\<close> by (auto simp: connectedin)
show ?thesis
unfolding connectedin connected_space_def
proof (intro conjI notI; clarify)
show "f x \<in> topspace Y" if "x \<in> S" for x
using \<open>S \<subseteq> topspace X\<close> continuous_map_image_subset_topspace f that by blast
next
fix U V
let ?U = "{x \<in> topspace X. f x \<in> U}"
let ?V = "{x \<in> topspace X. f x \<in> V}"
assume UV: "openin Y U" "openin Y V" "f ` S \<subseteq> U \<union> V" "U \<inter> V \<inter> f ` S = {}" "U \<inter> f ` S \<noteq> {}" "V \<inter> f ` S \<noteq> {}"
then have 1: "?U \<inter> ?V \<inter> S = {}"
by auto
have 2: "openin X ?U" "openin X ?V"
using \<open>openin Y U\<close> \<open>openin Y V\<close> continuous_map f by fastforce+
show "False"
using * [of ?U ?V] UV \<open>S \<subseteq> topspace X\<close>
by (auto simp: 1 2)
qed
qed
lemma homeomorphic_connected_space:
"X homeomorphic_space Y \<Longrightarrow> connected_space X \<longleftrightarrow> connected_space Y"
unfolding homeomorphic_space_def homeomorphic_maps_def
apply safe
apply (metis connectedin_continuous_map_image connected_space_subconnected continuous_map_image_subset_topspace image_eqI image_subset_iff)
by (metis (no_types, hide_lams) connectedin_continuous_map_image connectedin_topspace continuous_map_def continuous_map_image_subset_topspace imageI set_eq_subset subsetI)
lemma homeomorphic_map_connectedness:
assumes f: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
shows "connectedin Y (f ` U) \<longleftrightarrow> connectedin X U"
proof -
have 1: "f ` U \<subseteq> topspace Y \<longleftrightarrow> U \<subseteq> topspace X"
using U f homeomorphic_imp_surjective_map by blast
moreover have "connected_space (subtopology Y (f ` U)) \<longleftrightarrow> connected_space (subtopology X U)"
proof (rule homeomorphic_connected_space)
have "f ` U \<subseteq> topspace Y"
by (simp add: U 1)
then have "topspace Y \<inter> f ` U = f ` U"
by (simp add: subset_antisym)
then show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
by (metis (no_types) Int_subset_iff U f homeomorphic_map_imp_homeomorphic_space homeomorphic_map_subtopologies homeomorphic_space_sym subset_antisym subset_refl)
qed
ultimately show ?thesis
by (auto simp: connectedin_def)
qed
lemma homeomorphic_map_connectedness_eq:
"homeomorphic_map X Y f
\<Longrightarrow> connectedin X U \<longleftrightarrow>
U \<subseteq> topspace X \<and> connectedin Y (f ` U)"
using homeomorphic_map_connectedness connectedin_subset_topspace by metis
lemma connectedin_discrete_topology:
"connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
proof (cases "S \<subseteq> U")
case True
show ?thesis
proof (cases "S = {}")
case False
moreover have "connectedin (discrete_topology U) S \<longleftrightarrow> (\<exists>a. S = {a})"
apply safe
using False connectedin_inter_frontier_of insert_Diff apply fastforce
using True by auto
ultimately show ?thesis
by auto
qed simp
next
case False
then show ?thesis
by (simp add: connectedin_def)
qed
lemma connected_space_discrete_topology:
"connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
by (metis connectedin_discrete_topology connectedin_topspace order_refl topspace_discrete_topology)
subsection\<open>Compact sets\<close>
definition compactin where
"compactin X S \<longleftrightarrow>
S \<subseteq> topspace X \<and>
(\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> S \<subseteq> \<Union>\<U>
\<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>))"
definition compact_space where
"compact_space X \<equiv> compactin X (topspace X)"
lemma compact_space_alt:
"compact_space X \<longleftrightarrow>
(\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> topspace X \<subseteq> \<Union>\<U>
\<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>))"
by (simp add: compact_space_def compactin_def)
lemma compact_space:
"compact_space X \<longleftrightarrow>
(\<forall>\<U>. (\<forall>U \<in> \<U>. openin X U) \<and> \<Union>\<U> = topspace X
\<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> \<Union>\<F> = topspace X))"
unfolding compact_space_alt
using openin_subset by fastforce
lemma compactin_euclideanreal_iff [simp]: "compactin euclideanreal S \<longleftrightarrow> compact S"
by (simp add: compact_eq_Heine_Borel compactin_def) meson
lemma compactin_absolute [simp]:
"compactin (subtopology X S) S \<longleftrightarrow> compactin X S"
proof -
have eq: "(\<forall>U \<in> \<U>. \<exists>Y. openin X Y \<and> U = Y \<inter> S) \<longleftrightarrow> \<U> \<subseteq> (\<lambda>Y. Y \<inter> S) ` {y. openin X y}" for \<U>
by auto
show ?thesis
by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image exists_finite_subset_image)
qed
lemma compactin_subspace: "compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> compact_space (subtopology X S)"
unfolding compact_space_def topspace_subtopology
by (metis compactin_absolute compactin_def inf.absorb2)
lemma compact_space_subtopology: "compactin X S \<Longrightarrow> compact_space (subtopology X S)"
by (simp add: compactin_subspace)
lemma compactin_subtopology: "compactin (subtopology X S) T \<longleftrightarrow> compactin X T \<and> T \<subseteq> S"
apply (simp add: compactin_subspace topspace_subtopology)
by (metis inf.orderE inf_commute subtopology_subtopology)
lemma compactin_subset_topspace: "compactin X S \<Longrightarrow> S \<subseteq> topspace X"
by (simp add: compactin_subspace)
lemma compactin_contractive:
"\<lbrakk>compactin X' S; topspace X' = topspace X;
\<And>U. openin X U \<Longrightarrow> openin X' U\<rbrakk> \<Longrightarrow> compactin X S"
by (simp add: compactin_def)
lemma finite_imp_compactin:
"\<lbrakk>S \<subseteq> topspace X; finite S\<rbrakk> \<Longrightarrow> compactin X S"
by (metis compactin_subspace compact_space finite_UnionD inf.absorb_iff2 order_refl topspace_subtopology)
lemma compactin_empty [iff]: "compactin X {}"
by (simp add: finite_imp_compactin)
lemma compact_space_topspace_empty:
"topspace X = {} \<Longrightarrow> compact_space X"
by (simp add: compact_space_def)
lemma finite_imp_compactin_eq:
"finite S \<Longrightarrow> (compactin X S \<longleftrightarrow> S \<subseteq> topspace X)"
using compactin_subset_topspace finite_imp_compactin by blast
lemma compactin_sing [simp]: "compactin X {a} \<longleftrightarrow> a \<in> topspace X"
by (simp add: finite_imp_compactin_eq)
lemma closed_compactin:
assumes XK: "compactin X K" and "C \<subseteq> K" and XC: "closedin X C"
shows "compactin X C"
unfolding compactin_def
proof (intro conjI allI impI)
show "C \<subseteq> topspace X"
by (simp add: XC closedin_subset)
next
fix \<U> :: "'a set set"
assume \<U>: "Ball \<U> (openin X) \<and> C \<subseteq> \<Union>\<U>"
have "(\<forall>U\<in>insert (topspace X - C) \<U>. openin X U)"
using XC \<U> by blast
moreover have "K \<subseteq> \<Union>insert (topspace X - C) \<U>"
using \<U> XK compactin_subset_topspace by fastforce
ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> insert (topspace X - C) \<U>" "K \<subseteq> \<Union>\<F>"
using assms unfolding compactin_def by metis
moreover have "openin X (topspace X - C)"
using XC by auto
ultimately show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> C \<subseteq> \<Union>\<F>"
using \<open>C \<subseteq> K\<close>
by (rule_tac x="\<F> - {topspace X - C}" in exI) auto
qed
lemma closedin_compact_space:
"\<lbrakk>compact_space X; closedin X S\<rbrakk> \<Longrightarrow> compactin X S"
by (simp add: closed_compactin closedin_subset compact_space_def)
lemma compact_Int_closedin:
assumes "compactin X S" "closedin X T" shows "compactin X (S \<inter> T)"
proof -
have "compactin (subtopology X S) (S \<inter> T)"
by (metis assms closedin_compact_space closedin_subtopology compactin_subspace inf_commute)
then show ?thesis
by (simp add: compactin_subtopology)
qed
lemma closed_Int_compactin: "\<lbrakk>closedin X S; compactin X T\<rbrakk> \<Longrightarrow> compactin X (S \<inter> T)"
by (metis compact_Int_closedin inf_commute)
lemma compactin_Un:
assumes S: "compactin X S" and T: "compactin X T" shows "compactin X (S \<union> T)"
unfolding compactin_def
proof (intro conjI allI impI)
show "S \<union> T \<subseteq> topspace X"
using assms by (auto simp: compactin_def)
next
fix \<U> :: "'a set set"
assume \<U>: "Ball \<U> (openin X) \<and> S \<union> T \<subseteq> \<Union>\<U>"
with S obtain \<F> where \<V>: "finite \<F>" "\<F> \<subseteq> \<U>" "S \<subseteq> \<Union>\<F>"
unfolding compactin_def by (meson sup.bounded_iff)
obtain \<W> where "finite \<W>" "\<W> \<subseteq> \<U>" "T \<subseteq> \<Union>\<W>"
using \<U> T
unfolding compactin_def by (meson sup.bounded_iff)
with \<V> show "\<exists>\<V>. finite \<V> \<and> \<V> \<subseteq> \<U> \<and> S \<union> T \<subseteq> \<Union>\<V>"
by (rule_tac x="\<F> \<union> \<W>" in exI) auto
qed
lemma compactin_Union:
"\<lbrakk>finite \<F>; \<And>S. S \<in> \<F> \<Longrightarrow> compactin X S\<rbrakk> \<Longrightarrow> compactin X (\<Union>\<F>)"
by (induction rule: finite_induct) (simp_all add: compactin_Un)
lemma compactin_subtopology_imp_compact:
assumes "compactin (subtopology X S) K" shows "compactin X K"
using assms
proof (clarsimp simp add: compactin_def topspace_subtopology)
fix \<U>
define \<V> where "\<V> \<equiv> (\<lambda>U. U \<inter> S) ` \<U>"
assume "K \<subseteq> topspace X" and "K \<subseteq> S" and "\<forall>x\<in>\<U>. openin X x" and "K \<subseteq> \<Union>\<U>"
then have "\<forall>V \<in> \<V>. openin (subtopology X S) V" "K \<subseteq> \<Union>\<V>"
unfolding \<V>_def by (auto simp: openin_subtopology)
moreover
assume "\<forall>\<U>. (\<forall>x\<in>\<U>. openin (subtopology X S) x) \<and> K \<subseteq> \<Union>\<U> \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>)"
ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
by meson
then have \<F>: "\<exists>U. U \<in> \<U> \<and> V = U \<inter> S" if "V \<in> \<F>" for V
unfolding \<V>_def using that by blast
let ?\<F> = "(\<lambda>F. @U. U \<in> \<U> \<and> F = U \<inter> S) ` \<F>"
show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
proof (intro exI conjI)
show "finite ?\<F>"
using \<open>finite \<F>\<close> by blast
show "?\<F> \<subseteq> \<U>"
using someI_ex [OF \<F>] by blast
show "K \<subseteq> \<Union>?\<F>"
proof clarsimp
fix x
assume "x \<in> K"
then show "\<exists>V \<in> \<F>. x \<in> (SOME U. U \<in> \<U> \<and> V = U \<inter> S)"
using \<open>K \<subseteq> \<Union>\<F>\<close> someI_ex [OF \<F>]
by (metis (no_types, lifting) IntD1 Union_iff subsetCE)
qed
qed
qed
lemma compact_imp_compactin_subtopology:
assumes "compactin X K" "K \<subseteq> S" shows "compactin (subtopology X S) K"
using assms
proof (clarsimp simp add: compactin_def topspace_subtopology)
fix \<U> :: "'a set set"
define \<V> where "\<V> \<equiv> {V. openin X V \<and> (\<exists>U \<in> \<U>. U = V \<inter> S)}"
assume "K \<subseteq> S" and "K \<subseteq> topspace X" and "\<forall>U\<in>\<U>. openin (subtopology X S) U" and "K \<subseteq> \<Union>\<U>"
then have "\<forall>V \<in> \<V>. openin X V" "K \<subseteq> \<Union>\<V>"
unfolding \<V>_def by (fastforce simp: subset_eq openin_subtopology)+
moreover
assume "\<forall>\<U>. (\<forall>U\<in>\<U>. openin X U) \<and> K \<subseteq> \<Union>\<U> \<longrightarrow> (\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>)"
ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<V>" "K \<subseteq> \<Union>\<F>"
by meson
let ?\<F> = "(\<lambda>F. F \<inter> S) ` \<F>"
show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union>\<F>"
proof (intro exI conjI)
show "finite ?\<F>"
using \<open>finite \<F>\<close> by blast
show "?\<F> \<subseteq> \<U>"
using \<V>_def \<open>\<F> \<subseteq> \<V>\<close> by blast
show "K \<subseteq> \<Union>?\<F>"
using \<open>K \<subseteq> \<Union>\<F>\<close> assms(2) by auto
qed
qed
proposition compact_space_fip:
"compact_space X \<longleftrightarrow>
(\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
(is "_ = ?rhs")
proof (cases "topspace X = {}")
case True
then show ?thesis
apply (clarsimp simp add: compact_space_def closedin_topspace_empty)
by (metis finite.emptyI finite_insert infinite_super insertI1 subsetI)
next
case False
show ?thesis
proof safe
fix \<U> :: "'a set set"
assume * [rule_format]: "\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}"
define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
assume clo: "\<forall>C\<in>\<U>. closedin X C" and [simp]: "\<Inter>\<U> = {}"
then have "\<forall>V \<in> \<V>. openin X V" "topspace X \<subseteq> \<Union>\<V>"
by (auto simp: \<V>_def)
moreover assume [unfolded compact_space_alt, rule_format, of \<V>]: "compact_space X"
ultimately obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<U>" "topspace X \<subseteq> topspace X - \<Inter>\<F>"
by (auto simp: exists_finite_subset_image \<V>_def)
moreover have "\<F> \<noteq> {}"
using \<F> \<open>topspace X \<noteq> {}\<close> by blast
ultimately show "False"
using * [of \<F>]
by auto (metis Diff_iff Inter_iff clo closedin_def subsetD)
next
assume R [rule_format]: ?rhs
show "compact_space X"
unfolding compact_space_alt
proof clarify
fix \<U> :: "'a set set"
define \<V> where "\<V> \<equiv> (\<lambda>S. topspace X - S) ` \<U>"
assume "\<forall>C\<in>\<U>. openin X C" and "topspace X \<subseteq> \<Union>\<U>"
with \<open>topspace X \<noteq> {}\<close> have *: "\<forall>V \<in> \<V>. closedin X V" "\<U> \<noteq> {}"
by (auto simp: \<V>_def)
show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> topspace X \<subseteq> \<Union>\<F>"
proof (rule ccontr; simp)
assume "\<forall>\<F>\<subseteq>\<U>. finite \<F> \<longrightarrow> \<not> topspace X \<subseteq> \<Union>\<F>"
then have "\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<V> \<longrightarrow> \<Inter>\<F> \<noteq> {}"
by (simp add: \<V>_def all_finite_subset_image)
with \<open>topspace X \<subseteq> \<Union>\<U>\<close> show False
using R [of \<V>] * by (simp add: \<V>_def)
qed
qed
qed
qed
corollary compactin_fip:
"compactin X S \<longleftrightarrow>
S \<subseteq> topspace X \<and>
(\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"
proof (cases "S = {}")
case False
show ?thesis
proof (cases "S \<subseteq> topspace X")
case True
then have "compactin X S \<longleftrightarrow>
(\<forall>\<U>. \<U> \<subseteq> (\<lambda>T. S \<inter> T) ` {T. closedin X T} \<longrightarrow>
(\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
by (simp add: compact_space_fip compactin_subspace closedin_subtopology image_def subset_eq Int_commute imp_conjL)
also have "\<dots> = (\<forall>\<U>\<subseteq>Collect (closedin X). (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> (\<inter>) S ` \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {})"
by (simp add: all_subset_image)
also have "\<dots> = (\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"
proof -
have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter> ((\<inter>) S ` \<F>) \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {}) \<longleftrightarrow>
((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})" for \<U>
by simp (use \<open>S \<noteq> {}\<close> in blast)
show ?thesis
apply (simp only: imp_conjL [symmetric] all_finite_subset_image eq)
apply (simp add: subset_eq)
done
qed
finally show ?thesis
using True by simp
qed (simp add: compactin_subspace)
qed force
corollary compact_space_imp_nest:
fixes C :: "nat \<Rightarrow> 'a set"
assumes "compact_space X" and clo: "\<And>n. closedin X (C n)"
and ne: "\<And>n. C n \<noteq> {}" and inc: "\<And>m n. m \<le> n \<Longrightarrow> C n \<subseteq> C m"
shows "(\<Inter>n. C n) \<noteq> {}"
proof -
let ?\<U> = "range (\<lambda>n. \<Inter>m \<le> n. C m)"
have "closedin X A" if "A \<in> ?\<U>" for A
using that clo by auto
moreover have "(\<Inter>n\<in>K. \<Inter>m \<le> n. C m) \<noteq> {}" if "finite K" for K
proof -
obtain n where "\<And>k. k \<in> K \<Longrightarrow> k \<le> n"
using Max.coboundedI \<open>finite K\<close> by blast
with inc have "C n \<subseteq> (\<Inter>n\<in>K. \<Inter>m \<le> n. C m)"
by blast
with ne [of n] show ?thesis
by blast
qed
ultimately show ?thesis
using \<open>compact_space X\<close> [unfolded compact_space_fip, rule_format, of ?\<U>]
by (simp add: all_finite_subset_image INT_extend_simps UN_atMost_UNIV del: INT_simps)
qed
lemma compactin_discrete_topology:
"compactin (discrete_topology X) S \<longleftrightarrow> S \<subseteq> X \<and> finite S" (is "?lhs = ?rhs")
proof (intro iffI conjI)
assume L: ?lhs
then show "S \<subseteq> X"
by (auto simp: compactin_def)
have *: "\<And>\<U>. Ball \<U> (openin (discrete_topology X)) \<and> S \<subseteq> \<Union>\<U> \<Longrightarrow>
(\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>)"
using L by (auto simp: compactin_def)
show "finite S"
using * [of "(\<lambda>x. {x}) ` X"] \<open>S \<subseteq> X\<close>
by clarsimp (metis UN_singleton finite_subset_image infinite_super)
next
assume ?rhs
then show ?lhs
by (simp add: finite_imp_compactin)
qed
lemma compact_space_discrete_topology: "compact_space(discrete_topology X) \<longleftrightarrow> finite X"
by (simp add: compactin_discrete_topology compact_space_def)
lemma compact_space_imp_Bolzano_Weierstrass:
assumes "compact_space X" "infinite S" "S \<subseteq> topspace X"
shows "X derived_set_of S \<noteq> {}"
proof
assume X: "X derived_set_of S = {}"
then have "closedin X S"
by (simp add: closedin_contains_derived_set assms)
then have "compactin X S"
by (rule closedin_compact_space [OF \<open>compact_space X\<close>])
with X show False
by (metis \<open>infinite S\<close> compactin_subspace compact_space_discrete_topology inf_bot_right subtopology_eq_discrete_topology_eq)
qed
lemma compactin_imp_Bolzano_Weierstrass:
"\<lbrakk>compactin X S; infinite T \<and> T \<subseteq> S\<rbrakk> \<Longrightarrow> S \<inter> X derived_set_of T \<noteq> {}"
using compact_space_imp_Bolzano_Weierstrass [of "subtopology X S"]
by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2 topspace_subtopology)
lemma compact_closure_of_imp_Bolzano_Weierstrass:
"\<lbrakk>compactin X (X closure_of S); infinite T; T \<subseteq> S; T \<subseteq> topspace X\<rbrakk> \<Longrightarrow> X derived_set_of T \<noteq> {}"
using closure_of_mono closure_of_subset compactin_imp_Bolzano_Weierstrass by fastforce
lemma discrete_compactin_eq_finite:
"S \<inter> X derived_set_of S = {} \<Longrightarrow> compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> finite S"
apply (rule iffI)
using compactin_imp_Bolzano_Weierstrass compactin_subset_topspace apply blast
by (simp add: finite_imp_compactin_eq)
lemma discrete_compact_space_eq_finite:
"X derived_set_of (topspace X) = {} \<Longrightarrow> (compact_space X \<longleftrightarrow> finite(topspace X))"
by (metis compact_space_discrete_topology discrete_topology_unique_derived_set)
lemma image_compactin:
assumes cpt: "compactin X S" and cont: "continuous_map X Y f"
shows "compactin Y (f ` S)"
unfolding compactin_def
proof (intro conjI allI impI)
show "f ` S \<subseteq> topspace Y"
using compactin_subset_topspace cont continuous_map_image_subset_topspace cpt by blast
next
fix \<U> :: "'b set set"
assume \<U>: "Ball \<U> (openin Y) \<and> f ` S \<subseteq> \<Union>\<U>"
define \<V> where "\<V> \<equiv> (\<lambda>U. {x \<in> topspace X. f x \<in> U}) ` \<U>"
have "S \<subseteq> topspace X"
and *: "\<And>\<U>. \<lbrakk>\<forall>U\<in>\<U>. openin X U; S \<subseteq> \<Union>\<U>\<rbrakk> \<Longrightarrow> \<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> S \<subseteq> \<Union>\<F>"
using cpt by (auto simp: compactin_def)
obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<V>" "S \<subseteq> \<Union>\<F>"
proof -
have 1: "\<forall>U\<in>\<V>. openin X U"
unfolding \<V>_def using \<U> cont[unfolded continuous_map] by blast
have 2: "S \<subseteq> \<Union>\<V>"
unfolding \<V>_def using compactin_subset_topspace cpt \<U> by fastforce
show thesis
using * [OF 1 2] that by metis
qed
have "\<forall>v \<in> \<V>. \<exists>U. U \<in> \<U> \<and> v = {x \<in> topspace X. f x \<in> U}"
using \<V>_def by blast
then obtain U where U: "\<forall>v \<in> \<V>. U v \<in> \<U> \<and> v = {x \<in> topspace X. f x \<in> U v}"
by metis
show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> f ` S \<subseteq> \<Union>\<F>"
proof (intro conjI exI)
show "finite (U ` \<F>)"
by (simp add: \<open>finite \<F>\<close>)
next
show "U ` \<F> \<subseteq> \<U>"
using \<open>\<F> \<subseteq> \<V>\<close> U by auto
next
show "f ` S \<subseteq> \<Union> (U ` \<F>)"
using \<F>(2-3) U UnionE subset_eq U by fastforce
qed
qed
lemma homeomorphic_compact_space:
assumes "X homeomorphic_space Y"
shows "compact_space X \<longleftrightarrow> compact_space Y"
using homeomorphic_space_sym
by (metis assms compact_space_def homeomorphic_eq_everything_map homeomorphic_space image_compactin)
lemma homeomorphic_map_compactness:
assumes hom: "homeomorphic_map X Y f" and U: "U \<subseteq> topspace X"
shows "compactin Y (f ` U) \<longleftrightarrow> compactin X U"
proof -
have "f ` U \<subseteq> topspace Y"
using hom U homeomorphic_imp_surjective_map by blast
moreover have "homeomorphic_map (subtopology X U) (subtopology Y (f ` U)) f"
using U hom homeomorphic_imp_surjective_map by (blast intro: homeomorphic_map_subtopologies)
then have "compact_space (subtopology Y (f ` U)) = compact_space (subtopology X U)"
using homeomorphic_compact_space homeomorphic_map_imp_homeomorphic_space by blast
ultimately show ?thesis
by (simp add: compactin_subspace U)
qed
lemma homeomorphic_map_compactness_eq:
"homeomorphic_map X Y f
\<Longrightarrow> compactin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> compactin Y (f ` U)"
by (meson compactin_subset_topspace homeomorphic_map_compactness)
subsection\<open>Embedding maps\<close>
definition embedding_map
where "embedding_map X Y f \<equiv> homeomorphic_map X (subtopology Y (f ` (topspace X))) f"
lemma embedding_map_eq:
"\<lbrakk>embedding_map X Y f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> embedding_map X Y g"
unfolding embedding_map_def
by (metis homeomorphic_map_eq image_cong)
lemma embedding_map_compose:
assumes "embedding_map X X' f" "embedding_map X' X'' g"
shows "embedding_map X X'' (g \<circ> f)"
proof -
have hm: "homeomorphic_map X (subtopology X' (f ` topspace X)) f" "homeomorphic_map X' (subtopology X'' (g ` topspace X')) g"
using assms by (auto simp: embedding_map_def)
then obtain C where "g ` topspace X' \<inter> C = (g \<circ> f) ` topspace X"
by (metis (no_types) Int_absorb1 continuous_map_image_subset_topspace continuous_map_in_subtopology homeomorphic_eq_everything_map image_comp image_mono)
then have "homeomorphic_map (subtopology X' (f ` topspace X)) (subtopology X'' ((g \<circ> f) ` topspace X)) g"
by (metis hm homeomorphic_imp_surjective_map homeomorphic_map_subtopologies image_comp subtopology_subtopology topspace_subtopology)
then show ?thesis
unfolding embedding_map_def
using hm(1) homeomorphic_map_compose by blast
qed
lemma surjective_embedding_map:
"embedding_map X Y f \<and> f ` (topspace X) = topspace Y \<longleftrightarrow> homeomorphic_map X Y f"
by (force simp: embedding_map_def homeomorphic_eq_everything_map)
lemma embedding_map_in_subtopology:
"embedding_map X (subtopology Y S) f \<longleftrightarrow> embedding_map X Y f \<and> f ` (topspace X) \<subseteq> S"
apply (auto simp: embedding_map_def subtopology_subtopology Int_absorb1)
apply (metis (no_types) homeomorphic_imp_surjective_map subtopology_subtopology subtopology_topspace topspace_subtopology)
apply (simp add: continuous_map_def homeomorphic_eq_everything_map topspace_subtopology)
done
lemma injective_open_imp_embedding_map:
"\<lbrakk>continuous_map X Y f; open_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
unfolding embedding_map_def
apply (rule bijective_open_imp_homeomorphic_map)
using continuous_map_in_subtopology apply blast
apply (auto simp: continuous_map_in_subtopology open_map_into_subtopology topspace_subtopology continuous_map)
done
lemma injective_closed_imp_embedding_map:
"\<lbrakk>continuous_map X Y f; closed_map X Y f; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> embedding_map X Y f"
unfolding embedding_map_def
apply (rule bijective_closed_imp_homeomorphic_map)
apply (simp_all add: continuous_map_into_subtopology closed_map_into_subtopology)
apply (simp add: continuous_map inf.absorb_iff2 topspace_subtopology)
done
lemma embedding_map_imp_homeomorphic_space:
"embedding_map X Y f \<Longrightarrow> X homeomorphic_space (subtopology Y (f ` (topspace X)))"
unfolding embedding_map_def
using homeomorphic_space by blast
subsection \<open>Continuity\<close>
lemma continuous_on_open:
"continuous_on S f \<longleftrightarrow>
(\<forall>T. openin (subtopology euclidean (f ` S)) T \<longrightarrow>
openin (subtopology euclidean S) (S \<inter> f -` T))"
unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
lemma continuous_on_closed:
"continuous_on S f \<longleftrightarrow>
(\<forall>T. closedin (subtopology euclidean (f ` S)) T \<longrightarrow>
closedin (subtopology euclidean S) (S \<inter> f -` T))"
unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
lemma continuous_on_imp_closedin:
assumes "continuous_on S f" "closedin (subtopology euclidean (f ` S)) T"
shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
using assms continuous_on_closed by blast
subsection%unimportant \<open>Half-global and completely global cases\<close>
lemma continuous_openin_preimage_gen:
assumes "continuous_on S f" "open T"
shows "openin (subtopology euclidean S) (S \<inter> f -` T)"
proof -
have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
by auto
have "openin (subtopology euclidean (f ` S)) (T \<inter> f ` S)"
using openin_open_Int[of T "f ` S", OF assms(2)] unfolding openin_open by auto
then show ?thesis
using assms(1)[unfolded continuous_on_open, THEN spec[where x="T \<inter> f ` S"]]
using * by auto
qed
lemma continuous_closedin_preimage:
assumes "continuous_on S f" and "closed T"
shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
proof -
have *: "(S \<inter> f -` T) = (S \<inter> f -` (T \<inter> f ` S))"
by auto
have "closedin (subtopology euclidean (f ` S)) (T \<inter> f ` S)"
using closedin_closed_Int[of T "f ` S", OF assms(2)]
by (simp add: Int_commute)
then show ?thesis
using assms(1)[unfolded continuous_on_closed, THEN spec[where x="T \<inter> f ` S"]]
using * by auto
qed
lemma continuous_openin_preimage_eq:
"continuous_on S f \<longleftrightarrow>
(\<forall>T. open T \<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T))"
apply safe
apply (simp add: continuous_openin_preimage_gen)
apply (fastforce simp add: continuous_on_open openin_open)
done
lemma continuous_closedin_preimage_eq:
"continuous_on S f \<longleftrightarrow>
(\<forall>T. closed T \<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` T))"
apply safe
apply (simp add: continuous_closedin_preimage)
apply (fastforce simp add: continuous_on_closed closedin_closed)
done
lemma continuous_open_preimage:
assumes contf: "continuous_on S f" and "open S" "open T"
shows "open (S \<inter> f -` T)"
proof-
obtain U where "open U" "(S \<inter> f -` T) = S \<inter> U"
using continuous_openin_preimage_gen[OF contf \<open>open T\<close>]
unfolding openin_open by auto
then show ?thesis
using open_Int[of S U, OF \<open>open S\<close>] by auto
qed
lemma continuous_closed_preimage:
assumes contf: "continuous_on S f" and "closed S" "closed T"
shows "closed (S \<inter> f -` T)"
proof-
obtain U where "closed U" "(S \<inter> f -` T) = S \<inter> U"
using continuous_closedin_preimage[OF contf \<open>closed T\<close>]
unfolding closedin_closed by auto
then show ?thesis using closed_Int[of S U, OF \<open>closed S\<close>] by auto
qed
lemma continuous_open_vimage: "open S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` S)"
by (metis continuous_on_eq_continuous_within open_vimage)
lemma continuous_closed_vimage: "closed S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> closed (f -` S)"
by (simp add: closed_vimage continuous_on_eq_continuous_within)
lemma Times_in_interior_subtopology:
assumes "(x, y) \<in> U" "openin (subtopology euclidean (S \<times> T)) U"
obtains V W where "openin (subtopology euclidean S) V" "x \<in> V"
"openin (subtopology euclidean T) W" "y \<in> W" "(V \<times> W) \<subseteq> U"
proof -
from assms obtain E where "open E" "U = S \<times> T \<inter> E" "(x, y) \<in> E" "x \<in> S" "y \<in> T"
by (auto simp: openin_open)
from open_prod_elim[OF \<open>open E\<close> \<open>(x, y) \<in> E\<close>]
obtain E1 E2 where "open E1" "open E2" "(x, y) \<in> E1 \<times> E2" "E1 \<times> E2 \<subseteq> E"
by blast
show ?thesis
proof
show "openin (subtopology euclidean S) (E1 \<inter> S)"
"openin (subtopology euclidean T) (E2 \<inter> T)"
using \<open>open E1\<close> \<open>open E2\<close>
by (auto simp: openin_open)
show "x \<in> E1 \<inter> S" "y \<in> E2 \<inter> T"
using \<open>(x, y) \<in> E1 \<times> E2\<close> \<open>x \<in> S\<close> \<open>y \<in> T\<close> by auto
show "(E1 \<inter> S) \<times> (E2 \<inter> T) \<subseteq> U"
using \<open>E1 \<times> E2 \<subseteq> E\<close> \<open>U = _\<close>
by (auto simp: )
qed
qed
lemma closedin_Times:
"closedin (subtopology euclidean S) S' \<Longrightarrow> closedin (subtopology euclidean T) T' \<Longrightarrow>
closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
unfolding closedin_closed using closed_Times by blast
lemma openin_Times:
"openin (subtopology euclidean S) S' \<Longrightarrow> openin (subtopology euclidean T) T' \<Longrightarrow>
openin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
unfolding openin_open using open_Times by blast
lemma openin_Times_eq:
fixes S :: "'a::topological_space set" and T :: "'b::topological_space set"
shows
"openin (subtopology euclidean (S \<times> T)) (S' \<times> T') \<longleftrightarrow>
S' = {} \<or> T' = {} \<or> openin (subtopology euclidean S) S' \<and> openin (subtopology euclidean T) T'"
(is "?lhs = ?rhs")
proof (cases "S' = {} \<or> T' = {}")
case True
then show ?thesis by auto
next
case False
then obtain x y where "x \<in> S'" "y \<in> T'"
by blast
show ?thesis
proof
assume ?lhs
have "openin (subtopology euclidean S) S'"
apply (subst openin_subopen, clarify)
apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
using \<open>y \<in> T'\<close>
apply auto
done
moreover have "openin (subtopology euclidean T) T'"
apply (subst openin_subopen, clarify)
apply (rule Times_in_interior_subtopology [OF _ \<open>?lhs\<close>])
using \<open>x \<in> S'\<close>
apply auto
done
ultimately show ?rhs
by simp
next
assume ?rhs
with False show ?lhs
by (simp add: openin_Times)
qed
qed
lemma Lim_transform_within_openin:
assumes f: "(f \<longlongrightarrow> l) (at a within T)"
and "openin (subtopology euclidean T) S" "a \<in> S"
and eq: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> a\<rbrakk> \<Longrightarrow> f x = g x"
shows "(g \<longlongrightarrow> l) (at a within T)"
proof -
have "\<forall>\<^sub>F x in at a within T. x \<in> T \<and> x \<noteq> a"
by (simp add: eventually_at_filter)
moreover
from \<open>openin _ _\<close> obtain U where "open U" "S = T \<inter> U"
by (auto simp: openin_open)
then have "a \<in> U" using \<open>a \<in> S\<close> by auto
from topological_tendstoD[OF tendsto_ident_at \<open>open U\<close> \<open>a \<in> U\<close>]
have "\<forall>\<^sub>F x in at a within T. x \<in> U" by auto
ultimately
have "\<forall>\<^sub>F x in at a within T. f x = g x"
by eventually_elim (auto simp: \<open>S = _\<close> eq)
then show ?thesis using f
by (rule Lim_transform_eventually)
qed
lemma continuous_on_open_gen:
assumes "f ` S \<subseteq> T"
shows "continuous_on S f \<longleftrightarrow>
(\<forall>U. openin (subtopology euclidean T) U
\<longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (clarsimp simp add: continuous_openin_preimage_eq openin_open)
(metis Int_assoc assms image_subset_iff_subset_vimage inf.absorb_iff1)
next
assume R [rule_format]: ?rhs
show ?lhs
proof (clarsimp simp add: continuous_openin_preimage_eq)
fix U::"'a set"
assume "open U"
then have "openin (subtopology euclidean S) (S \<inter> f -` (U \<inter> T))"
by (metis R inf_commute openin_open)
then show "openin (subtopology euclidean S) (S \<inter> f -` U)"
by (metis Int_assoc Int_commute assms image_subset_iff_subset_vimage inf.absorb_iff2 vimage_Int)
qed
qed
lemma continuous_openin_preimage:
"\<lbrakk>continuous_on S f; f ` S \<subseteq> T; openin (subtopology euclidean T) U\<rbrakk>
\<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` U)"
by (simp add: continuous_on_open_gen)
lemma continuous_on_closed_gen:
assumes "f ` S \<subseteq> T"
shows "continuous_on S f \<longleftrightarrow>
(\<forall>U. closedin (subtopology euclidean T) U
\<longrightarrow> closedin (subtopology euclidean S) (S \<inter> f -` U))"
(is "?lhs = ?rhs")
proof -
have *: "U \<subseteq> T \<Longrightarrow> S \<inter> f -` (T - U) = S - (S \<inter> f -` U)" for U
using assms by blast
show ?thesis
proof
assume L: ?lhs
show ?rhs
proof clarify
fix U
assume "closedin (subtopology euclidean T) U"
then show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
using L unfolding continuous_on_open_gen [OF assms]
by (metis * closedin_def inf_le1 topspace_euclidean_subtopology)
qed
next
assume R [rule_format]: ?rhs
show ?lhs
unfolding continuous_on_open_gen [OF assms]
by (metis * R inf_le1 openin_closedin_eq topspace_euclidean_subtopology)
qed
qed
lemma continuous_closedin_preimage_gen:
assumes "continuous_on S f" "f ` S \<subseteq> T" "closedin (subtopology euclidean T) U"
shows "closedin (subtopology euclidean S) (S \<inter> f -` U)"
using assms continuous_on_closed_gen by blast
lemma continuous_transform_within_openin:
assumes "continuous (at a within T) f"
and "openin (subtopology euclidean T) S" "a \<in> S"
and eq: "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
shows "continuous (at a within T) g"
using assms by (simp add: Lim_transform_within_openin continuous_within)
end