Simplicial complexes and triangulations; Baire Category Theorem
authorpaulson <lp15@cam.ac.uk>
Fri Sep 08 12:49:40 2017 +0100 (20 months ago)
changeset 66641ff2e0115fea4
parent 66640 c61c957b0439
child 66642 88f86bcba5b3
child 66643 f7e38b8583a0
Simplicial complexes and triangulations; Baire Category Theorem
NEWS
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Polytope.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/NEWS	Fri Sep 08 11:09:56 2017 +0200
     1.2 +++ b/NEWS	Fri Sep 08 12:49:40 2017 +0100
     1.3 @@ -254,8 +254,8 @@
     1.4  * Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.
     1.5  
     1.6  * Session HOL-Analysis: more material involving arcs, paths, covering
     1.7 -spaces, innessential maps, retracts, material on infinite products.
     1.8 -Major results include the Jordan Curve Theorem and the Great Picard
     1.9 +spaces, innessential maps, retracts, infinite products, simplicial complexes.
    1.10 +Baire Category theory. Major results include the Jordan Curve Theorem and the Great Picard
    1.11  Theorem.
    1.12  
    1.13  * Session HOL-Algebra has been extended by additional lattice theory:
     2.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Sep 08 11:09:56 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Sep 08 12:49:40 2017 +0100
     2.3 @@ -3979,6 +3979,41 @@
     2.4    shows "aff_dim S < 0 \<longleftrightarrow>S = {}"
     2.5  by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq)
     2.6  
     2.7 +lemma aff_lowdim_subset_hyperplane:
     2.8 +  fixes S :: "'a::euclidean_space set"
     2.9 +  assumes "aff_dim S < DIM('a)"
    2.10 +  obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x = b}"
    2.11 +proof (cases "S={}")
    2.12 +  case True
    2.13 +  moreover
    2.14 +  have "(SOME b. b \<in> Basis) \<noteq> 0"
    2.15 +    by (metis norm_some_Basis norm_zero zero_neq_one)
    2.16 +  ultimately show ?thesis
    2.17 +    using that by blast
    2.18 +next
    2.19 +  case False
    2.20 +  then obtain c S' where "c \<notin> S'" "S = insert c S'"
    2.21 +    by (meson equals0I mk_disjoint_insert)
    2.22 +  have "dim (op + (-c) ` S) < DIM('a)"
    2.23 +    by (metis \<open>S = insert c S'\<close> aff_dim_eq_dim assms hull_inc insertI1 of_nat_less_imp_less)
    2.24 +  then obtain a where "a \<noteq> 0" "span (op + (-c) ` S) \<subseteq> {x. a \<bullet> x = 0}"
    2.25 +    using lowdim_subset_hyperplane by blast
    2.26 +  moreover
    2.27 +  have "a \<bullet> w = a \<bullet> c" if "span (op + (- c) ` S) \<subseteq> {x. a \<bullet> x = 0}" "w \<in> S" for w
    2.28 +  proof -
    2.29 +    have "w-c \<in> span (op + (- c) ` S)"
    2.30 +      by (simp add: span_superset \<open>w \<in> S\<close>)
    2.31 +    with that have "w-c \<in> {x. a \<bullet> x = 0}"
    2.32 +      by blast
    2.33 +    then show ?thesis
    2.34 +      by (auto simp: algebra_simps)
    2.35 +  qed
    2.36 +  ultimately have "S \<subseteq> {x. a \<bullet> x = a \<bullet> c}"
    2.37 +    by blast
    2.38 +  then show ?thesis
    2.39 +    by (rule that[OF \<open>a \<noteq> 0\<close>])
    2.40 +qed
    2.41 +
    2.42  lemma affine_independent_card_dim_diffs:
    2.43    fixes S :: "'a :: euclidean_space set"
    2.44    assumes "~ affine_dependent S" "a \<in> S"
     3.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Fri Sep 08 11:09:56 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Sep 08 12:49:40 2017 +0100
     3.3 @@ -310,7 +310,7 @@
     3.4  lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
     3.5    unfolding span_def by (rule hull_minimal)
     3.6  
     3.7 -lemma span_UNIV: "span UNIV = UNIV"
     3.8 +lemma span_UNIV [simp]: "span UNIV = UNIV"
     3.9    by (intro span_unique) auto
    3.10  
    3.11  lemma (in real_vector) span_induct:
     4.1 --- a/src/HOL/Analysis/Polytope.thy	Fri Sep 08 11:09:56 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Polytope.thy	Fri Sep 08 12:49:40 2017 +0100
     4.3 @@ -3811,4 +3811,113 @@
     4.4    qed
     4.5  qed
     4.6  
     4.7 +subsection\<open>Some results on cell division with full-dimensional cells only\<close>
     4.8 +
     4.9 +lemma convex_Union_fulldim_cells:
    4.10 +  assumes "finite \<S>" and clo: "\<And>C. C \<in> \<S> \<Longrightarrow> closed C" and con: "\<And>C. C \<in> \<S> \<Longrightarrow> convex C"
    4.11 +      and eq: "\<Union>\<S> = U"and  "convex U"
    4.12 + shows "\<Union>{C \<in> \<S>. aff_dim C = aff_dim U} = U"  (is "?lhs = U")
    4.13 +proof -
    4.14 +  have "closed U"
    4.15 +    using \<open>finite \<S>\<close> clo eq by blast
    4.16 +  have "?lhs \<subseteq> U"
    4.17 +    using eq by blast
    4.18 +  moreover have "U \<subseteq> ?lhs"
    4.19 +  proof (cases "\<forall>C \<in> \<S>. aff_dim C = aff_dim U")
    4.20 +    case True
    4.21 +    then show ?thesis
    4.22 +      using eq by blast
    4.23 +  next
    4.24 +    case False
    4.25 +    have "closed ?lhs"
    4.26 +      by (simp add: \<open>finite \<S>\<close> clo closed_Union)
    4.27 +    moreover have "U \<subseteq> closure ?lhs"
    4.28 +    proof -
    4.29 +      have "U \<subseteq> closure(\<Inter>{U - C |C. C \<in> \<S> \<and> aff_dim C < aff_dim U})"
    4.30 +      proof (rule Baire [OF \<open>closed U\<close>])
    4.31 +        show "countable {U - C |C. C \<in> \<S> \<and> aff_dim C < aff_dim U}"
    4.32 +          using \<open>finite \<S>\<close> uncountable_infinite by fastforce
    4.33 +        have "\<And>C. C \<in> \<S> \<Longrightarrow> openin (subtopology euclidean U) (U-C)"
    4.34 +          by (metis Sup_upper clo closed_limpt closedin_limpt eq openin_diff openin_subtopology_self)
    4.35 +        then show "openin (subtopology euclidean U) T \<and> U \<subseteq> closure T"
    4.36 +          if "T \<in> {U - C |C. C \<in> \<S> \<and> aff_dim C < aff_dim U}" for T
    4.37 +          using that dense_complement_convex_closed \<open>closed U\<close> \<open>convex U\<close> by auto
    4.38 +      qed
    4.39 +      also have "... \<subseteq> closure ?lhs"
    4.40 +      proof -
    4.41 +        obtain C where "C \<in> \<S>" "aff_dim C < aff_dim U"
    4.42 +          by (metis False Sup_upper aff_dim_subset eq eq_iff not_le)
    4.43 +        have "\<exists>X. X \<in> \<S> \<and> aff_dim X = aff_dim U \<and> x \<in> X"
    4.44 +          if "\<And>V. (\<exists>C. V = U - C \<and> C \<in> \<S> \<and> aff_dim C < aff_dim U) \<Longrightarrow> x \<in> V" for x
    4.45 +        proof -
    4.46 +          have "x \<in> U \<and> x \<in> \<Union>\<S>"
    4.47 +            using \<open>C \<in> \<S>\<close> \<open>aff_dim C < aff_dim U\<close> eq that by blast
    4.48 +          then show ?thesis
    4.49 +            by (metis Diff_iff Sup_upper Union_iff aff_dim_subset dual_order.order_iff_strict eq that)
    4.50 +        qed
    4.51 +        then show ?thesis
    4.52 +          by (auto intro!: closure_mono)
    4.53 +      qed
    4.54 +      finally show ?thesis .
    4.55 +    qed
    4.56 +    ultimately show ?thesis
    4.57 +      using closure_subset_eq by blast
    4.58 +  qed
    4.59 +  ultimately show ?thesis by blast
    4.60 +qed
    4.61 +
    4.62 +proposition fine_triangular_subdivision_of_cell_complex:
    4.63 +  assumes "0 < e" "finite \<M>"
    4.64 +      and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
    4.65 +      and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = d"
    4.66 +      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
    4.67 +  obtains \<T> where "triangulation \<T>" "\<And>k. k \<in> \<T> \<Longrightarrow> diameter k < e"
    4.68 +                 "\<And>k. k \<in> \<T> \<Longrightarrow> aff_dim k = d" "\<Union>\<T> = \<Union>\<M>"
    4.69 +                 "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>f. finite f \<and> f \<subseteq> \<T> \<and> C = \<Union>f"
    4.70 +                 "\<And>k. k \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> k \<subseteq> C"
    4.71 +proof -
    4.72 +  obtain \<T> where "simplicial_complex \<T>"
    4.73 +             and dia\<T>: "\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
    4.74 +             and "\<Union>\<T> = \<Union>\<M>"
    4.75 +             and in\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
    4.76 +             and in\<T>: "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
    4.77 +    by (blast intro: fine_simplicial_subdivision_of_cell_complex [OF \<open>e > 0\<close> \<open>finite \<M>\<close> poly face])
    4.78 +  let ?\<T> = "{K \<in> \<T>. aff_dim K = d}"
    4.79 +  show thesis
    4.80 +  proof
    4.81 +    show "triangulation ?\<T>"
    4.82 +      using \<open>simplicial_complex \<T>\<close> by (auto simp: triangulation_def simplicial_complex_def)
    4.83 +    show "diameter L < e" if "L \<in> {K \<in> \<T>. aff_dim K = d}" for L
    4.84 +      using that by (auto simp: dia\<T>)
    4.85 +    show "aff_dim L = d" if "L \<in> {K \<in> \<T>. aff_dim K = d}" for L
    4.86 +      using that by auto
    4.87 +    show "\<exists>F. finite F \<and> F \<subseteq> {K \<in> \<T>. aff_dim K = d} \<and> C = \<Union>F" if "C \<in> \<M>" for C
    4.88 +    proof -
    4.89 +      obtain F where "finite F" "F \<subseteq> \<T>" "C = \<Union>F"
    4.90 +        using in\<M> [OF \<open>C \<in> \<M>\<close>] by auto
    4.91 +      show ?thesis
    4.92 +      proof (intro exI conjI)
    4.93 +        show "finite {K \<in> F. aff_dim K = d}"
    4.94 +          by (simp add: \<open>finite F\<close>)
    4.95 +        show "{K \<in> F. aff_dim K = d} \<subseteq> {K \<in> \<T>. aff_dim K = d}"
    4.96 +          using \<open>F \<subseteq> \<T>\<close> by blast
    4.97 +        have "d = aff_dim C"
    4.98 +          by (simp add: aff that)
    4.99 +        moreover have "\<And>K. K \<in> F \<Longrightarrow> closed K \<and> convex K"
   4.100 +          using \<open>simplicial_complex \<T>\<close> \<open>F \<subseteq> \<T>\<close>
   4.101 +          unfolding simplicial_complex_def by (metis subsetCE \<open>F \<subseteq> \<T>\<close> closed_simplex convex_simplex)
   4.102 +        moreover have "convex (\<Union>F)"
   4.103 +          using \<open>C = \<Union>F\<close> poly polytope_imp_convex that by blast
   4.104 +        ultimately show "C = \<Union>{K \<in> F. aff_dim K = d}"
   4.105 +          by (simp add: convex_Union_fulldim_cells \<open>C = \<Union>F\<close> \<open>finite F\<close>)
   4.106 +      qed
   4.107 +    qed
   4.108 +    then show "\<Union>{K \<in> \<T>. aff_dim K = d} = \<Union>\<M>"
   4.109 +      by auto (meson in\<T> subsetCE)
   4.110 +    show "\<exists>C. C \<in> \<M> \<and> L \<subseteq> C"
   4.111 +      if "L \<in> {K \<in> \<T>. aff_dim K = d}" for L
   4.112 +      using that by (auto simp: in\<T>)
   4.113 +  qed
   4.114 +qed
   4.115 +
   4.116  end
     5.1 --- a/src/HOL/Analysis/Starlike.thy	Fri Sep 08 11:09:56 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Starlike.thy	Fri Sep 08 12:49:40 2017 +0100
     5.3 @@ -7041,6 +7041,70 @@
     5.4      by (rule that [OF 1 2 3 4 5 6])
     5.5  qed
     5.6  
     5.7 +
     5.8 +proposition orthogonal_to_subspace_exists_gen:
     5.9 +  fixes S :: "'a :: euclidean_space set"
    5.10 +  assumes "span S \<subset> span T"
    5.11 +  obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
    5.12 +proof -
    5.13 +  obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
    5.14 +             and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
    5.15 +             and "independent B" "card B = dim S" "span B = span S"
    5.16 +    by (rule orthonormal_basis_subspace [of "span S"]) auto
    5.17 +  with assms obtain u where spanBT: "span B \<subseteq> span T" and "u \<notin> span B" "u \<in> span T"
    5.18 +    by auto
    5.19 +  obtain C where orthBC: "pairwise orthogonal (B \<union> C)" and spanBC: "span (B \<union> C) = span (B \<union> {u})"
    5.20 +    by (blast intro: orthogonal_extension [OF orthB])
    5.21 +  show thesis
    5.22 +  proof (cases "C \<subseteq> insert 0 B")
    5.23 +    case True
    5.24 +    then have "C \<subseteq> span B"
    5.25 +      using Linear_Algebra.span_eq
    5.26 +      by (metis span_insert_0 subset_trans)
    5.27 +    moreover have "u \<in> span (B \<union> C)"
    5.28 +      using \<open>span (B \<union> C) = span (B \<union> {u})\<close> span_inc by force
    5.29 +    ultimately show ?thesis
    5.30 +      by (metis \<open>u \<notin> span B\<close> span_Un span_span sup.orderE)
    5.31 +  next
    5.32 +    case False
    5.33 +    then obtain x where "x \<in> C" "x \<noteq> 0" "x \<notin> B"
    5.34 +      by blast
    5.35 +    then have "x \<in> span T"
    5.36 +      by (metis (no_types, lifting) Un_insert_right Un_upper2 \<open>u \<in> span T\<close> spanBT spanBC \<open>u \<in> span T\<close> insert_subset span_inc span_mono span_span subsetCE subset_trans sup_bot.comm_neutral)
    5.37 +    moreover have "orthogonal x y" if "y \<in> span B" for y
    5.38 +      using that
    5.39 +    proof (rule span_induct)
    5.40 +      show "subspace {a. orthogonal x a}"
    5.41 +        by (simp add: subspace_orthogonal_to_vector)
    5.42 +      show "\<And>b. b \<in> B \<Longrightarrow> orthogonal x b"
    5.43 +        by (metis Un_iff \<open>x \<in> C\<close> \<open>x \<notin> B\<close> orthBC pairwise_def)
    5.44 +    qed
    5.45 +    ultimately show ?thesis
    5.46 +      using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto
    5.47 +  qed
    5.48 +qed
    5.49 +
    5.50 +corollary orthogonal_to_subspace_exists:
    5.51 +  fixes S :: "'a :: euclidean_space set"
    5.52 +  assumes "dim S < DIM('a)"
    5.53 +  obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
    5.54 +proof -
    5.55 +have "span S \<subset> UNIV"
    5.56 +  by (metis assms dim_eq_full less_irrefl top.not_eq_extremum)
    5.57 +  with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis by auto
    5.58 +qed
    5.59 +
    5.60 +corollary orthogonal_to_vector_exists:
    5.61 +  fixes x :: "'a :: euclidean_space"
    5.62 +  assumes "2 \<le> DIM('a)"
    5.63 +  obtains y where "y \<noteq> 0" "orthogonal x y"
    5.64 +proof -
    5.65 +  have "dim {x} < DIM('a)"
    5.66 +    using assms by auto
    5.67 +  then show thesis
    5.68 +    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_clauses(1) that)
    5.69 +qed
    5.70 +
    5.71  proposition orthogonal_subspace_decomp_exists:
    5.72    fixes S :: "'a :: euclidean_space set"
    5.73    obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
    5.74 @@ -7202,6 +7266,119 @@
    5.75    finally show "dim T \<le> dim S" by simp
    5.76  qed
    5.77  
    5.78 +subsection\<open>Lower-dimensional affine subsets are nowhere dense.\<close>
    5.79 +
    5.80 +proposition dense_complement_subspace:
    5.81 +  fixes S :: "'a :: euclidean_space set"
    5.82 +  assumes dim_less: "dim T < dim S" and "subspace S" shows "closure(S - T) = S"
    5.83 +proof -
    5.84 +  have "closure(S - U) = S" if "dim U < dim S" "U \<subseteq> S" for U
    5.85 +  proof -
    5.86 +    have "span U \<subset> span S"
    5.87 +      by (metis neq_iff psubsetI span_eq_dim span_mono that)
    5.88 +    then obtain a where "a \<noteq> 0" "a \<in> span S" and a: "\<And>y. y \<in> span U \<Longrightarrow> orthogonal a y"
    5.89 +      using orthogonal_to_subspace_exists_gen by metis
    5.90 +    show ?thesis
    5.91 +    proof
    5.92 +      have "closed S"
    5.93 +        by (simp add: \<open>subspace S\<close> closed_subspace)
    5.94 +      then show "closure (S - U) \<subseteq> S"
    5.95 +        by (simp add: Diff_subset closure_minimal)
    5.96 +      show "S \<subseteq> closure (S - U)"
    5.97 +      proof (clarsimp simp: closure_approachable)
    5.98 +        fix x and e::real
    5.99 +        assume "x \<in> S" "0 < e"
   5.100 +        show "\<exists>y\<in>S - U. dist y x < e"
   5.101 +        proof (cases "x \<in> U")
   5.102 +          case True
   5.103 +          let ?y = "x + (e/2 / norm a) *\<^sub>R a"
   5.104 +          show ?thesis
   5.105 +          proof
   5.106 +            show "dist ?y x < e"
   5.107 +              using \<open>0 < e\<close> by (simp add: dist_norm)
   5.108 +          next
   5.109 +            have "?y \<in> S"
   5.110 +              by (metis span_eq \<open>a \<in> span S\<close> \<open>x \<in> S\<close> \<open>subspace S\<close> subspace_add subspace_mul)
   5.111 +            moreover have "?y \<notin> U"
   5.112 +            proof -
   5.113 +              have "e/2 / norm a \<noteq> 0"
   5.114 +                using \<open>0 < e\<close> \<open>a \<noteq> 0\<close> by auto
   5.115 +              then show ?thesis
   5.116 +                by (metis True \<open>a \<noteq> 0\<close> a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_clauses(1))
   5.117 +            qed
   5.118 +            ultimately show "?y \<in> S - U" by blast
   5.119 +          qed
   5.120 +        next
   5.121 +          case False
   5.122 +          with \<open>0 < e\<close> \<open>x \<in> S\<close> show ?thesis by force
   5.123 +        qed
   5.124 +      qed
   5.125 +    qed
   5.126 +  qed
   5.127 +  moreover have "S - S \<inter> T = S-T"
   5.128 +    by blast
   5.129 +  moreover have "dim (S \<inter> T) < dim S"
   5.130 +    by (metis dim_less dim_subset inf.cobounded2 inf.orderE inf.strict_boundedE not_le)
   5.131 +  ultimately show ?thesis
   5.132 +    by force
   5.133 +qed
   5.134 +
   5.135 +corollary dense_complement_affine:
   5.136 +  fixes S :: "'a :: euclidean_space set"
   5.137 +  assumes less: "aff_dim T < aff_dim S" and "affine S" shows "closure(S - T) = S"
   5.138 +proof (cases "S \<inter> T = {}")
   5.139 +  case True
   5.140 +  then show ?thesis
   5.141 +    by (metis Diff_triv affine_hull_eq \<open>affine S\<close> closure_same_affine_hull closure_subset hull_subset subset_antisym)
   5.142 +next
   5.143 +  case False
   5.144 +  then obtain z where z: "z \<in> S \<inter> T" by blast
   5.145 +  then have "subspace (op + (- z) ` S)"
   5.146 +    by (meson IntD1 affine_diffs_subspace \<open>affine S\<close>)
   5.147 +  moreover have "int (dim (op + (- z) ` T)) < int (dim (op + (- z) ` S))"
   5.148 +    using z less by (simp add: aff_dim_eq_dim [symmetric] hull_inc)
   5.149 +  ultimately have "closure((op + (- z) ` S) - (op + (- z) ` T)) = (op + (- z) ` S)"
   5.150 +    by (simp add: dense_complement_subspace)
   5.151 +  then show ?thesis
   5.152 +    by (metis closure_translation translation_diff translation_invert)
   5.153 +qed
   5.154 +
   5.155 +corollary dense_complement_openin_affine_hull:
   5.156 +  fixes S :: "'a :: euclidean_space set"
   5.157 +  assumes less: "aff_dim T < aff_dim S"
   5.158 +      and ope: "openin (subtopology euclidean (affine hull S)) S"
   5.159 +    shows "closure(S - T) = closure S"
   5.160 +proof -
   5.161 +  have "affine hull S - T \<subseteq> affine hull S"
   5.162 +    by blast
   5.163 +  then have "closure (S \<inter> closure (affine hull S - T)) = closure (S \<inter> (affine hull S - T))"
   5.164 +    by (rule closure_openin_Int_closure [OF ope])
   5.165 +  then show ?thesis
   5.166 +    by (metis Int_Diff aff_dim_affine_hull affine_affine_hull dense_complement_affine hull_subset inf.orderE less)
   5.167 +qed
   5.168 +
   5.169 +corollary dense_complement_convex:
   5.170 +  fixes S :: "'a :: euclidean_space set"
   5.171 +  assumes "aff_dim T < aff_dim S" "convex S"
   5.172 +    shows "closure(S - T) = closure S"
   5.173 +proof
   5.174 +  show "closure (S - T) \<subseteq> closure S"
   5.175 +    by (simp add: Diff_subset closure_mono)
   5.176 +  have "closure (rel_interior S - T) = closure (rel_interior S)"
   5.177 +    apply (rule dense_complement_openin_affine_hull)
   5.178 +    apply (simp add: assms rel_interior_aff_dim)
   5.179 +    using \<open>convex S\<close> rel_interior_rel_open rel_open by blast
   5.180 +  then show "closure S \<subseteq> closure (S - T)"
   5.181 +    by (metis Diff_mono \<open>convex S\<close> closure_mono convex_closure_rel_interior order_refl rel_interior_subset)
   5.182 +qed
   5.183 +
   5.184 +corollary dense_complement_convex_closed:
   5.185 +  fixes S :: "'a :: euclidean_space set"
   5.186 +  assumes "aff_dim T < aff_dim S" "convex S" "closed S"
   5.187 +    shows "closure(S - T) = S"
   5.188 +  by (simp add: assms dense_complement_convex)
   5.189 +
   5.190 +
   5.191  subsection\<open>Parallel slices, etc.\<close>
   5.192  
   5.193  text\<open> If we take a slice out of a set, we can do it perpendicularly,
     6.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Sep 08 11:09:56 2017 +0200
     6.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Sep 08 12:49:40 2017 +0100
     6.3 @@ -2356,6 +2356,28 @@
     6.4      done
     6.5  qed
     6.6  
     6.7 +lemma closure_openin_Int_closure:
     6.8 +  assumes ope: "openin (subtopology euclidean U) S" and "T \<subseteq> U"
     6.9 +  shows "closure(S \<inter> closure T) = closure(S \<inter> T)"
    6.10 +proof
    6.11 +  obtain V where "open V" and S: "S = U \<inter> V"
    6.12 +    using ope using openin_open by metis
    6.13 +  show "closure (S \<inter> closure T) \<subseteq> closure (S \<inter> T)"
    6.14 +    proof (clarsimp simp: S)
    6.15 +      fix x
    6.16 +      assume  "x \<in> closure (U \<inter> V \<inter> closure T)"
    6.17 +      then have "V \<inter> closure T \<subseteq> A \<Longrightarrow> x \<in> closure A" for A
    6.18 +          by (metis closure_mono subsetD inf.coboundedI2 inf_assoc)
    6.19 +      then have "x \<in> closure (T \<inter> V)"
    6.20 +         by (metis \<open>open V\<close> closure_closure inf_commute open_Int_closure_subset)
    6.21 +      then show "x \<in> closure (U \<inter> V \<inter> T)"
    6.22 +        by (metis \<open>T \<subseteq> U\<close> inf.absorb_iff2 inf_assoc inf_commute)
    6.23 +    qed
    6.24 +next
    6.25 +  show "closure (S \<inter> T) \<subseteq> closure (S \<inter> closure T)"
    6.26 +    by (meson Int_mono closure_mono closure_subset order_refl)
    6.27 +qed
    6.28 +
    6.29  lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
    6.30    unfolding closure_def using islimpt_punctured by blast
    6.31  
    6.32 @@ -3520,6 +3542,12 @@
    6.33    apply (metis dist_self)
    6.34    done
    6.35  
    6.36 +lemma closure_approachable_le:
    6.37 +  fixes S :: "'a::metric_space set"
    6.38 +  shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x \<le> e)"
    6.39 +  unfolding closure_approachable
    6.40 +  using dense by force
    6.41 +
    6.42  lemma closed_approachable:
    6.43    fixes S :: "'a::metric_space set"
    6.44    shows "closed S \<Longrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
    6.45 @@ -3544,6 +3572,17 @@
    6.46    then show ?thesis unfolding closure_approachable by auto
    6.47  qed
    6.48  
    6.49 +lemma closure_Int_ballI:
    6.50 +  fixes S :: "'a :: metric_space set"
    6.51 +  assumes "\<And>U. \<lbrakk>openin (subtopology euclidean S) U; U \<noteq> {}\<rbrakk> \<Longrightarrow> T \<inter> U \<noteq> {}"
    6.52 + shows "S \<subseteq> closure T"
    6.53 +proof (clarsimp simp: closure_approachable dist_commute)
    6.54 +  fix x and e::real
    6.55 +  assume "x \<in> S" "0 < e"
    6.56 +  with assms [of "S \<inter> ball x e"] show "\<exists>y\<in>T. dist x y < e"
    6.57 +    by force
    6.58 +qed
    6.59 +
    6.60  lemma closed_contains_Inf:
    6.61    fixes S :: "real set"
    6.62    shows "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> closed S \<Longrightarrow> Inf S \<in> S"
    6.63 @@ -4802,6 +4841,11 @@
    6.64      by (simp add: closure_subset open_Compl)
    6.65  qed
    6.66  
    6.67 +corollary closure_Int_ball_not_empty:
    6.68 +  assumes "S \<subseteq> closure T" "x \<in> S" "r > 0"
    6.69 +  shows "T \<inter> ball x r \<noteq> {}"
    6.70 +  using assms centre_in_ball closure_iff_nhds_not_empty by blast
    6.71 +
    6.72  lemma compact_filter:
    6.73    "compact U \<longleftrightarrow> (\<forall>F. F \<noteq> bot \<longrightarrow> eventually (\<lambda>x. x \<in> U) F \<longrightarrow> (\<exists>x\<in>U. inf (nhds x) F \<noteq> bot))"
    6.74  proof (intro allI iffI impI compact_fip[THEN iffD2] notI)
    6.75 @@ -5630,6 +5674,115 @@
    6.76      done
    6.77  qed
    6.78  
    6.79 +text\<open>The Baire propery of dense sets\<close>
    6.80 +theorem Baire:
    6.81 +  fixes S::"'a::{real_normed_vector,heine_borel} set"
    6.82 +  assumes "closed S" "countable \<G>"
    6.83 +      and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
    6.84 + shows "S \<subseteq> closure(\<Inter>\<G>)"
    6.85 +proof (cases "\<G> = {}")
    6.86 +  case True
    6.87 +  then show ?thesis
    6.88 +    using closure_subset by auto
    6.89 +next
    6.90 +  let ?g = "from_nat_into \<G>"
    6.91 +  case False
    6.92 +  then have gin: "?g n \<in> \<G>" for n
    6.93 +    by (simp add: from_nat_into)
    6.94 +  show ?thesis
    6.95 +  proof (clarsimp simp: closure_approachable)
    6.96 +    fix x and e::real
    6.97 +    assume "x \<in> S" "0 < e"
    6.98 +    obtain TF where opeF: "\<And>n. openin (subtopology euclidean S) (TF n)" 
    6.99 +               and ne: "\<And>n. TF n \<noteq> {}" 
   6.100 +               and subg: "\<And>n. S \<inter> closure(TF n) \<subseteq> ?g n"
   6.101 +               and subball: "\<And>n. closure(TF n) \<subseteq> ball x e" 
   6.102 +               and decr: "\<And>n. TF(Suc n) \<subseteq> TF n"
   6.103 +    proof -
   6.104 +      have *: "\<exists>Y. (openin (subtopology euclidean S) Y \<and> Y \<noteq> {} \<and>
   6.105 +                   S \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> U" 
   6.106 +        if opeU: "openin (subtopology euclidean S) U" and "U \<noteq> {}" and cloU: "closure U \<subseteq> ball x e" for U n
   6.107 +      proof -
   6.108 +        obtain T where T: "open T" "U = T \<inter> S"
   6.109 +          using \<open>openin (subtopology euclidean S) U\<close> by (auto simp: openin_subtopology)
   6.110 +        with \<open>U \<noteq> {}\<close> have "T \<inter> closure (?g n) \<noteq> {}"
   6.111 +          using gin ope by fastforce
   6.112 +        then have "T \<inter> ?g n \<noteq> {}"
   6.113 +          using \<open>open T\<close> open_Int_closure_eq_empty by blast
   6.114 +        then obtain y where "y \<in> U" "y \<in> ?g n"
   6.115 +          using T ope [of "?g n", OF gin] by (blast dest:  openin_imp_subset)
   6.116 +        moreover have "openin (subtopology euclidean S) (U \<inter> ?g n)"
   6.117 +          using gin ope opeU by blast
   6.118 +        ultimately obtain d where U: "U \<inter> ?g n \<subseteq> S" and "d > 0" and d: "ball y d \<inter> S \<subseteq> U \<inter> ?g n"
   6.119 +          by (force simp add: openin_contains_ball)
   6.120 +        show ?thesis
   6.121 +        proof (intro exI conjI)
   6.122 +          show "openin (subtopology euclidean S) (S \<inter> ball y (d/2))"
   6.123 +            by (simp add: openin_open_Int)
   6.124 +          show "S \<inter> ball y (d/2) \<noteq> {}"
   6.125 +            using \<open>0 < d\<close> \<open>y \<in> U\<close> opeU openin_imp_subset by fastforce
   6.126 +          have "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> closure (ball y (d/2))"
   6.127 +            using closure_mono by blast
   6.128 +          also have "... \<subseteq> ?g n"
   6.129 +            using \<open>d > 0\<close> d by force
   6.130 +          finally show "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> ?g n" .
   6.131 +          have "closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> ball y d"
   6.132 +          proof -
   6.133 +            have "closure (ball y (d/2)) \<subseteq> ball y d"
   6.134 +              using \<open>d > 0\<close> by auto
   6.135 +            then have "closure (S \<inter> ball y (d/2)) \<subseteq> ball y d"
   6.136 +              by (meson closure_mono inf.cobounded2 subset_trans)
   6.137 +            then show ?thesis
   6.138 +              by (simp add: \<open>closed S\<close> closure_minimal)
   6.139 +          qed
   6.140 +          also have "...  \<subseteq> ball x e"
   6.141 +            using cloU closure_subset d by blast
   6.142 +          finally show "closure (S \<inter> ball y (d/2)) \<subseteq> ball x e" .
   6.143 +          show "S \<inter> ball y (d/2) \<subseteq> U"
   6.144 +            using ball_divide_subset_numeral d by blast
   6.145 +        qed
   6.146 +      qed
   6.147 +      let ?\<Phi> = "\<lambda>n X. openin (subtopology euclidean S) X \<and> X \<noteq> {} \<and> 
   6.148 +                      S \<inter> closure X \<subseteq> ?g n \<and> closure X \<subseteq> ball x e"
   6.149 +      have "closure (S \<inter> ball x (e / 2)) \<subseteq> closure(ball x (e/2))"
   6.150 +        by (simp add: closure_mono)
   6.151 +      also have "...  \<subseteq> ball x e"
   6.152 +        using \<open>e > 0\<close> by auto
   6.153 +      finally have "closure (S \<inter> ball x (e / 2)) \<subseteq> ball x e" .
   6.154 +      moreover have"openin (subtopology euclidean S) (S \<inter> ball x (e / 2))" "S \<inter> ball x (e / 2) \<noteq> {}"
   6.155 +        using \<open>0 < e\<close> \<open>x \<in> S\<close> by auto
   6.156 +      ultimately obtain Y where Y: "?\<Phi> 0 Y \<and> Y \<subseteq> S \<inter> ball x (e / 2)"
   6.157 +            using * [of "S \<inter> ball x (e/2)" 0] by metis
   6.158 +      show thesis
   6.159 +      proof (rule exE [OF dependent_nat_choice [of ?\<Phi> "\<lambda>n X Y. Y \<subseteq> X"]])
   6.160 +        show "\<exists>x. ?\<Phi> 0 x"
   6.161 +          using Y by auto
   6.162 +        show "\<exists>Y. ?\<Phi> (Suc n) Y \<and> Y \<subseteq> X" if "?\<Phi> n X" for X n
   6.163 +          using that by (blast intro: *)
   6.164 +      qed (use that in metis)
   6.165 +    qed
   6.166 +    have "(\<Inter>n. S \<inter> closure (TF n)) \<noteq> {}"
   6.167 +    proof (rule compact_nest)
   6.168 +      show "\<And>n. compact (S \<inter> closure (TF n))"
   6.169 +        by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF \<open>closed S\<close>])
   6.170 +      show "\<And>n. S \<inter> closure (TF n) \<noteq> {}" 
   6.171 +        by (metis Int_absorb1 opeF \<open>closed S\<close> closure_eq_empty closure_minimal ne openin_imp_subset)
   6.172 +      show "\<And>m n. m \<le> n \<Longrightarrow> S \<inter> closure (TF n) \<subseteq> S \<inter> closure (TF m)"
   6.173 +        by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le)
   6.174 +    qed
   6.175 +    moreover have "(\<Inter>n. S \<inter> closure (TF n)) \<subseteq> {y \<in> \<Inter>\<G>. dist y x < e}"
   6.176 +    proof (clarsimp, intro conjI)
   6.177 +      fix y
   6.178 +      assume "y \<in> S" and y: "\<forall>n. y \<in> closure (TF n)"
   6.179 +      then show "\<forall>T\<in>\<G>. y \<in> T"
   6.180 +        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] set_mp subg)
   6.181 +      show "dist y x < e"
   6.182 +        by (metis y dist_commute mem_ball subball subsetCE)
   6.183 +    qed
   6.184 +    ultimately show "\<exists>y \<in> \<Inter>\<G>. dist y x < e"
   6.185 +      by auto
   6.186 +  qed
   6.187 +qed
   6.188  
   6.189  subsubsection \<open>Completeness\<close>
   6.190