src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44365 5daa55003649
parent 44342 8321948340ea
child 44457 d366fa5551ef
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 21 11:03:15 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 21 12:22:31 2011 -0700
     1.3 @@ -622,6 +622,23 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma interior_Times: "interior (A \<times> B) = interior A \<times> interior B"
     1.8 +proof (rule interior_unique)
     1.9 +  show "interior A \<times> interior B \<subseteq> A \<times> B"
    1.10 +    by (intro Sigma_mono interior_subset)
    1.11 +  show "open (interior A \<times> interior B)"
    1.12 +    by (intro open_Times open_interior)
    1.13 +  show "\<forall>T. T \<subseteq> A \<times> B \<and> open T \<longrightarrow> T \<subseteq> interior A \<times> interior B"
    1.14 +    apply (simp add: open_prod_def, clarify)
    1.15 +    apply (drule (1) bspec, clarify, rename_tac C D)
    1.16 +    apply (simp add: interior_def, rule conjI)
    1.17 +    apply (rule_tac x=C in exI, clarsimp)
    1.18 +    apply (rule SigmaD1, erule subsetD, erule subsetD, erule (1) SigmaI)
    1.19 +    apply (rule_tac x=D in exI, clarsimp)
    1.20 +    apply (rule SigmaD2, erule subsetD, erule subsetD, erule (1) SigmaI)
    1.21 +    done
    1.22 +qed
    1.23 +
    1.24  
    1.25  subsection {* Closure of a Set *}
    1.26  
    1.27 @@ -793,6 +810,23 @@
    1.28    unfolding closure_interior
    1.29    by blast
    1.30  
    1.31 +lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
    1.32 +proof (intro closure_unique conjI)
    1.33 +  show "A \<times> B \<subseteq> closure A \<times> closure B"
    1.34 +    by (intro Sigma_mono closure_subset)
    1.35 +  show "closed (closure A \<times> closure B)"
    1.36 +    by (intro closed_Times closed_closure)
    1.37 +  show "\<forall>T. A \<times> B \<subseteq> T \<and> closed T \<longrightarrow> closure A \<times> closure B \<subseteq> T"
    1.38 +    apply (simp add: closed_def open_prod_def, clarify)
    1.39 +    apply (rule ccontr)
    1.40 +    apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
    1.41 +    apply (simp add: closure_interior interior_def)
    1.42 +    apply (drule_tac x=C in spec)
    1.43 +    apply (drule_tac x=D in spec)
    1.44 +    apply auto
    1.45 +    done
    1.46 +qed
    1.47 +
    1.48  
    1.49  subsection {* Frontier (aka boundary) *}
    1.50