src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 49711 e5aaae7eadc9
parent 48125 602dc0215954
child 49834 b27bbb021df1
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Oct 05 13:48:22 2012 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Oct 05 13:57:48 2012 +0200
     1.3 @@ -28,12 +28,14 @@
     1.4  
     1.5  lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
     1.6  proof-
     1.7 -  {assume "T1=T2" hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp}
     1.8 +  { assume "T1=T2"
     1.9 +    hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp }
    1.10    moreover
    1.11 -  {assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
    1.12 +  { assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
    1.13      hence "openin T1 = openin T2" by (simp add: fun_eq_iff)
    1.14      hence "topology (openin T1) = topology (openin T2)" by simp
    1.15 -    hence "T1 = T2" unfolding openin_inverse .}
    1.16 +    hence "T1 = T2" unfolding openin_inverse .
    1.17 +  }
    1.18    ultimately show ?thesis by blast
    1.19  qed
    1.20  
    1.21 @@ -66,9 +68,11 @@
    1.22  
    1.23  lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def)
    1.24  
    1.25 -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")
    1.26 +lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
    1.27 +  (is "?lhs \<longleftrightarrow> ?rhs")
    1.28  proof
    1.29 -  assume ?lhs then show ?rhs by auto
    1.30 +  assume ?lhs
    1.31 +  then show ?rhs by auto
    1.32  next
    1.33    assume H: ?rhs
    1.34    let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
    1.35 @@ -77,6 +81,7 @@
    1.36    finally show "openin U S" .
    1.37  qed
    1.38  
    1.39 +
    1.40  subsubsection {* Closed sets *}
    1.41  
    1.42  definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
    1.43 @@ -167,9 +172,11 @@
    1.44    apply (rule iffI, clarify)
    1.45    apply (frule openin_subset[of U])  apply blast
    1.46    apply (rule exI[where x="topspace U"])
    1.47 -  by auto
    1.48 -
    1.49 -lemma subtopology_superset: assumes UV: "topspace U \<subseteq> V"
    1.50 +  apply auto
    1.51 +  done
    1.52 +
    1.53 +lemma subtopology_superset:
    1.54 +  assumes UV: "topspace U \<subseteq> V"
    1.55    shows "subtopology U V = U"
    1.56  proof-
    1.57    {fix S