--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Oct 05 13:48:22 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Oct 05 13:57:48 2012 +0200
@@ -28,12 +28,14 @@
lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
proof-
- {assume "T1=T2" hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp}
+ { assume "T1=T2"
+ hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp }
moreover
- {assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
+ { assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
hence "openin T1 = openin T2" by (simp add: fun_eq_iff)
hence "topology (openin T1) = topology (openin T2)" by simp
- hence "T1 = T2" unfolding openin_inverse .}
+ hence "T1 = T2" unfolding openin_inverse .
+ }
ultimately show ?thesis by blast
qed
@@ -66,9 +68,11 @@
lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: 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")
+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
+ assume ?lhs
+ then show ?rhs by auto
next
assume H: ?rhs
let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
@@ -77,6 +81,7 @@
finally show "openin U S" .
qed
+
subsubsection {* Closed sets *}
definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
@@ -167,9 +172,11 @@
apply (rule iffI, clarify)
apply (frule openin_subset[of U]) apply blast
apply (rule exI[where x="topspace U"])
- by auto
-
-lemma subtopology_superset: assumes UV: "topspace U \<subseteq> V"
+ apply auto
+ done
+
+lemma subtopology_superset:
+ assumes UV: "topspace U \<subseteq> V"
shows "subtopology U V = U"
proof-
{fix S