--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Oct 17 14:19:07 2018 +0100
@@ -635,8 +635,8 @@
then show "T1 = T2" unfolding openin_inverse .
qed
-text\<open>Infer the "universe" from union of all sets in the topology.\<close>
-
+
+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>
@@ -778,7 +778,52 @@
qed
-subsubsection \<open>Subspace topology\<close>
+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: Diff_subset 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 U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
@@ -818,6 +863,19 @@
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)
@@ -927,7 +985,7 @@
by (simp add: closedin_subtopology) blast
-subsubsection \<open>The standard Euclidean topology\<close>
+subsection \<open>The standard Euclidean topology\<close>
definition%important euclidean :: "'a::topological_space topology"
where "euclidean = topology open"
@@ -958,7 +1016,25 @@
lemma openin_subtopology_self [simp]: "openin (subtopology euclidean S) S"
by (metis openin_topspace topspace_euclidean_subtopology)
-text \<open>Basic "localization" results are handy for connectedness.\<close>
+subsubsection\<open>The most basic facts about the usual topology and metric on R\<close>
+
+abbreviation euclideanreal :: "real topology"
+ where "euclideanreal \<equiv> topology open"
+
+lemma real_openin [simp]: "openin euclideanreal S = open S"
+ by (simp add: euclidean_def open_openin)
+
+lemma topspace_euclideanreal [simp]: "topspace euclideanreal = UNIV"
+ using openin_subset open_UNIV real_openin by blast
+
+lemma topspace_euclideanreal_subtopology [simp]:
+ "topspace (subtopology euclideanreal S) = S"
+ by (simp add: topspace_subtopology)
+
+lemma real_closedin [simp]: "closedin euclideanreal S = closed S"
+ by (simp add: closed_closedin euclidean_def)
+
+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)