# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1504871380 -3600
# Node ID ff2e0115fea4166cc93ce63b68b8a5bd78f0bd01
# Parent  c61c957b04394bbea59da7615b5bc81a0f425432
Simplicial complexes and triangulations; Baire Category Theorem

diff -r c61c957b0439 -r ff2e0115fea4 NEWS
--- a/NEWS	Fri Sep 08 11:09:56 2017 +0200
+++ b/NEWS	Fri Sep 08 12:49:40 2017 +0100
@@ -254,8 +254,8 @@
 * Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.
 
 * Session HOL-Analysis: more material involving arcs, paths, covering
-spaces, innessential maps, retracts, material on infinite products.
-Major results include the Jordan Curve Theorem and the Great Picard
+spaces, innessential maps, retracts, infinite products, simplicial complexes.
+Baire Category theory. Major results include the Jordan Curve Theorem and the Great Picard
 Theorem.
 
 * Session HOL-Algebra has been extended by additional lattice theory:
diff -r c61c957b0439 -r ff2e0115fea4 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Sep 08 11:09:56 2017 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Sep 08 12:49:40 2017 +0100
@@ -3979,6 +3979,41 @@
   shows "aff_dim S < 0 \<longleftrightarrow>S = {}"
 by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq)
 
+lemma aff_lowdim_subset_hyperplane:
+  fixes S :: "'a::euclidean_space set"
+  assumes "aff_dim S < DIM('a)"
+  obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x = b}"
+proof (cases "S={}")
+  case True
+  moreover
+  have "(SOME b. b \<in> Basis) \<noteq> 0"
+    by (metis norm_some_Basis norm_zero zero_neq_one)
+  ultimately show ?thesis
+    using that by blast
+next
+  case False
+  then obtain c S' where "c \<notin> S'" "S = insert c S'"
+    by (meson equals0I mk_disjoint_insert)
+  have "dim (op + (-c) ` S) < DIM('a)"
+    by (metis \<open>S = insert c S'\<close> aff_dim_eq_dim assms hull_inc insertI1 of_nat_less_imp_less)
+  then obtain a where "a \<noteq> 0" "span (op + (-c) ` S) \<subseteq> {x. a \<bullet> x = 0}"
+    using lowdim_subset_hyperplane by blast
+  moreover
+  have "a \<bullet> w = a \<bullet> c" if "span (op + (- c) ` S) \<subseteq> {x. a \<bullet> x = 0}" "w \<in> S" for w
+  proof -
+    have "w-c \<in> span (op + (- c) ` S)"
+      by (simp add: span_superset \<open>w \<in> S\<close>)
+    with that have "w-c \<in> {x. a \<bullet> x = 0}"
+      by blast
+    then show ?thesis
+      by (auto simp: algebra_simps)
+  qed
+  ultimately have "S \<subseteq> {x. a \<bullet> x = a \<bullet> c}"
+    by blast
+  then show ?thesis
+    by (rule that[OF \<open>a \<noteq> 0\<close>])
+qed
+
 lemma affine_independent_card_dim_diffs:
   fixes S :: "'a :: euclidean_space set"
   assumes "~ affine_dependent S" "a \<in> S"
diff -r c61c957b0439 -r ff2e0115fea4 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Fri Sep 08 11:09:56 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Sep 08 12:49:40 2017 +0100
@@ -310,7 +310,7 @@
 lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
   unfolding span_def by (rule hull_minimal)
 
-lemma span_UNIV: "span UNIV = UNIV"
+lemma span_UNIV [simp]: "span UNIV = UNIV"
   by (intro span_unique) auto
 
 lemma (in real_vector) span_induct:
diff -r c61c957b0439 -r ff2e0115fea4 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Fri Sep 08 11:09:56 2017 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Fri Sep 08 12:49:40 2017 +0100
@@ -3811,4 +3811,113 @@
   qed
 qed
 
+subsection\<open>Some results on cell division with full-dimensional cells only\<close>
+
+lemma convex_Union_fulldim_cells:
+  assumes "finite \<S>" and clo: "\<And>C. C \<in> \<S> \<Longrightarrow> closed C" and con: "\<And>C. C \<in> \<S> \<Longrightarrow> convex C"
+      and eq: "\<Union>\<S> = U"and  "convex U"
+ shows "\<Union>{C \<in> \<S>. aff_dim C = aff_dim U} = U"  (is "?lhs = U")
+proof -
+  have "closed U"
+    using \<open>finite \<S>\<close> clo eq by blast
+  have "?lhs \<subseteq> U"
+    using eq by blast
+  moreover have "U \<subseteq> ?lhs"
+  proof (cases "\<forall>C \<in> \<S>. aff_dim C = aff_dim U")
+    case True
+    then show ?thesis
+      using eq by blast
+  next
+    case False
+    have "closed ?lhs"
+      by (simp add: \<open>finite \<S>\<close> clo closed_Union)
+    moreover have "U \<subseteq> closure ?lhs"
+    proof -
+      have "U \<subseteq> closure(\<Inter>{U - C |C. C \<in> \<S> \<and> aff_dim C < aff_dim U})"
+      proof (rule Baire [OF \<open>closed U\<close>])
+        show "countable {U - C |C. C \<in> \<S> \<and> aff_dim C < aff_dim U}"
+          using \<open>finite \<S>\<close> uncountable_infinite by fastforce
+        have "\<And>C. C \<in> \<S> \<Longrightarrow> openin (subtopology euclidean U) (U-C)"
+          by (metis Sup_upper clo closed_limpt closedin_limpt eq openin_diff openin_subtopology_self)
+        then show "openin (subtopology euclidean U) T \<and> U \<subseteq> closure T"
+          if "T \<in> {U - C |C. C \<in> \<S> \<and> aff_dim C < aff_dim U}" for T
+          using that dense_complement_convex_closed \<open>closed U\<close> \<open>convex U\<close> by auto
+      qed
+      also have "... \<subseteq> closure ?lhs"
+      proof -
+        obtain C where "C \<in> \<S>" "aff_dim C < aff_dim U"
+          by (metis False Sup_upper aff_dim_subset eq eq_iff not_le)
+        have "\<exists>X. X \<in> \<S> \<and> aff_dim X = aff_dim U \<and> x \<in> X"
+          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
+        proof -
+          have "x \<in> U \<and> x \<in> \<Union>\<S>"
+            using \<open>C \<in> \<S>\<close> \<open>aff_dim C < aff_dim U\<close> eq that by blast
+          then show ?thesis
+            by (metis Diff_iff Sup_upper Union_iff aff_dim_subset dual_order.order_iff_strict eq that)
+        qed
+        then show ?thesis
+          by (auto intro!: closure_mono)
+      qed
+      finally show ?thesis .
+    qed
+    ultimately show ?thesis
+      using closure_subset_eq by blast
+  qed
+  ultimately show ?thesis by blast
+qed
+
+proposition fine_triangular_subdivision_of_cell_complex:
+  assumes "0 < e" "finite \<M>"
+      and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
+      and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = d"
+      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"
+  obtains \<T> where "triangulation \<T>" "\<And>k. k \<in> \<T> \<Longrightarrow> diameter k < e"
+                 "\<And>k. k \<in> \<T> \<Longrightarrow> aff_dim k = d" "\<Union>\<T> = \<Union>\<M>"
+                 "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>f. finite f \<and> f \<subseteq> \<T> \<and> C = \<Union>f"
+                 "\<And>k. k \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> k \<subseteq> C"
+proof -
+  obtain \<T> where "simplicial_complex \<T>"
+             and dia\<T>: "\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
+             and "\<Union>\<T> = \<Union>\<M>"
+             and in\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
+             and in\<T>: "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
+    by (blast intro: fine_simplicial_subdivision_of_cell_complex [OF \<open>e > 0\<close> \<open>finite \<M>\<close> poly face])
+  let ?\<T> = "{K \<in> \<T>. aff_dim K = d}"
+  show thesis
+  proof
+    show "triangulation ?\<T>"
+      using \<open>simplicial_complex \<T>\<close> by (auto simp: triangulation_def simplicial_complex_def)
+    show "diameter L < e" if "L \<in> {K \<in> \<T>. aff_dim K = d}" for L
+      using that by (auto simp: dia\<T>)
+    show "aff_dim L = d" if "L \<in> {K \<in> \<T>. aff_dim K = d}" for L
+      using that by auto
+    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
+    proof -
+      obtain F where "finite F" "F \<subseteq> \<T>" "C = \<Union>F"
+        using in\<M> [OF \<open>C \<in> \<M>\<close>] by auto
+      show ?thesis
+      proof (intro exI conjI)
+        show "finite {K \<in> F. aff_dim K = d}"
+          by (simp add: \<open>finite F\<close>)
+        show "{K \<in> F. aff_dim K = d} \<subseteq> {K \<in> \<T>. aff_dim K = d}"
+          using \<open>F \<subseteq> \<T>\<close> by blast
+        have "d = aff_dim C"
+          by (simp add: aff that)
+        moreover have "\<And>K. K \<in> F \<Longrightarrow> closed K \<and> convex K"
+          using \<open>simplicial_complex \<T>\<close> \<open>F \<subseteq> \<T>\<close>
+          unfolding simplicial_complex_def by (metis subsetCE \<open>F \<subseteq> \<T>\<close> closed_simplex convex_simplex)
+        moreover have "convex (\<Union>F)"
+          using \<open>C = \<Union>F\<close> poly polytope_imp_convex that by blast
+        ultimately show "C = \<Union>{K \<in> F. aff_dim K = d}"
+          by (simp add: convex_Union_fulldim_cells \<open>C = \<Union>F\<close> \<open>finite F\<close>)
+      qed
+    qed
+    then show "\<Union>{K \<in> \<T>. aff_dim K = d} = \<Union>\<M>"
+      by auto (meson in\<T> subsetCE)
+    show "\<exists>C. C \<in> \<M> \<and> L \<subseteq> C"
+      if "L \<in> {K \<in> \<T>. aff_dim K = d}" for L
+      using that by (auto simp: in\<T>)
+  qed
+qed
+
 end
diff -r c61c957b0439 -r ff2e0115fea4 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Fri Sep 08 11:09:56 2017 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Fri Sep 08 12:49:40 2017 +0100
@@ -7041,6 +7041,70 @@
     by (rule that [OF 1 2 3 4 5 6])
 qed
 
+
+proposition orthogonal_to_subspace_exists_gen:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "span S \<subset> span T"
+  obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
+proof -
+  obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
+             and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
+             and "independent B" "card B = dim S" "span B = span S"
+    by (rule orthonormal_basis_subspace [of "span S"]) auto
+  with assms obtain u where spanBT: "span B \<subseteq> span T" and "u \<notin> span B" "u \<in> span T"
+    by auto
+  obtain C where orthBC: "pairwise orthogonal (B \<union> C)" and spanBC: "span (B \<union> C) = span (B \<union> {u})"
+    by (blast intro: orthogonal_extension [OF orthB])
+  show thesis
+  proof (cases "C \<subseteq> insert 0 B")
+    case True
+    then have "C \<subseteq> span B"
+      using Linear_Algebra.span_eq
+      by (metis span_insert_0 subset_trans)
+    moreover have "u \<in> span (B \<union> C)"
+      using \<open>span (B \<union> C) = span (B \<union> {u})\<close> span_inc by force
+    ultimately show ?thesis
+      by (metis \<open>u \<notin> span B\<close> span_Un span_span sup.orderE)
+  next
+    case False
+    then obtain x where "x \<in> C" "x \<noteq> 0" "x \<notin> B"
+      by blast
+    then have "x \<in> span T"
+      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)
+    moreover have "orthogonal x y" if "y \<in> span B" for y
+      using that
+    proof (rule span_induct)
+      show "subspace {a. orthogonal x a}"
+        by (simp add: subspace_orthogonal_to_vector)
+      show "\<And>b. b \<in> B \<Longrightarrow> orthogonal x b"
+        by (metis Un_iff \<open>x \<in> C\<close> \<open>x \<notin> B\<close> orthBC pairwise_def)
+    qed
+    ultimately show ?thesis
+      using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto
+  qed
+qed
+
+corollary orthogonal_to_subspace_exists:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "dim S < DIM('a)"
+  obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
+proof -
+have "span S \<subset> UNIV"
+  by (metis assms dim_eq_full less_irrefl top.not_eq_extremum)
+  with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis by auto
+qed
+
+corollary orthogonal_to_vector_exists:
+  fixes x :: "'a :: euclidean_space"
+  assumes "2 \<le> DIM('a)"
+  obtains y where "y \<noteq> 0" "orthogonal x y"
+proof -
+  have "dim {x} < DIM('a)"
+    using assms by auto
+  then show thesis
+    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_clauses(1) that)
+qed
+
 proposition orthogonal_subspace_decomp_exists:
   fixes S :: "'a :: euclidean_space set"
   obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
@@ -7202,6 +7266,119 @@
   finally show "dim T \<le> dim S" by simp
 qed
 
+subsection\<open>Lower-dimensional affine subsets are nowhere dense.\<close>
+
+proposition dense_complement_subspace:
+  fixes S :: "'a :: euclidean_space set"
+  assumes dim_less: "dim T < dim S" and "subspace S" shows "closure(S - T) = S"
+proof -
+  have "closure(S - U) = S" if "dim U < dim S" "U \<subseteq> S" for U
+  proof -
+    have "span U \<subset> span S"
+      by (metis neq_iff psubsetI span_eq_dim span_mono that)
+    then obtain a where "a \<noteq> 0" "a \<in> span S" and a: "\<And>y. y \<in> span U \<Longrightarrow> orthogonal a y"
+      using orthogonal_to_subspace_exists_gen by metis
+    show ?thesis
+    proof
+      have "closed S"
+        by (simp add: \<open>subspace S\<close> closed_subspace)
+      then show "closure (S - U) \<subseteq> S"
+        by (simp add: Diff_subset closure_minimal)
+      show "S \<subseteq> closure (S - U)"
+      proof (clarsimp simp: closure_approachable)
+        fix x and e::real
+        assume "x \<in> S" "0 < e"
+        show "\<exists>y\<in>S - U. dist y x < e"
+        proof (cases "x \<in> U")
+          case True
+          let ?y = "x + (e/2 / norm a) *\<^sub>R a"
+          show ?thesis
+          proof
+            show "dist ?y x < e"
+              using \<open>0 < e\<close> by (simp add: dist_norm)
+          next
+            have "?y \<in> S"
+              by (metis span_eq \<open>a \<in> span S\<close> \<open>x \<in> S\<close> \<open>subspace S\<close> subspace_add subspace_mul)
+            moreover have "?y \<notin> U"
+            proof -
+              have "e/2 / norm a \<noteq> 0"
+                using \<open>0 < e\<close> \<open>a \<noteq> 0\<close> by auto
+              then show ?thesis
+                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))
+            qed
+            ultimately show "?y \<in> S - U" by blast
+          qed
+        next
+          case False
+          with \<open>0 < e\<close> \<open>x \<in> S\<close> show ?thesis by force
+        qed
+      qed
+    qed
+  qed
+  moreover have "S - S \<inter> T = S-T"
+    by blast
+  moreover have "dim (S \<inter> T) < dim S"
+    by (metis dim_less dim_subset inf.cobounded2 inf.orderE inf.strict_boundedE not_le)
+  ultimately show ?thesis
+    by force
+qed
+
+corollary dense_complement_affine:
+  fixes S :: "'a :: euclidean_space set"
+  assumes less: "aff_dim T < aff_dim S" and "affine S" shows "closure(S - T) = S"
+proof (cases "S \<inter> T = {}")
+  case True
+  then show ?thesis
+    by (metis Diff_triv affine_hull_eq \<open>affine S\<close> closure_same_affine_hull closure_subset hull_subset subset_antisym)
+next
+  case False
+  then obtain z where z: "z \<in> S \<inter> T" by blast
+  then have "subspace (op + (- z) ` S)"
+    by (meson IntD1 affine_diffs_subspace \<open>affine S\<close>)
+  moreover have "int (dim (op + (- z) ` T)) < int (dim (op + (- z) ` S))"
+    using z less by (simp add: aff_dim_eq_dim [symmetric] hull_inc)
+  ultimately have "closure((op + (- z) ` S) - (op + (- z) ` T)) = (op + (- z) ` S)"
+    by (simp add: dense_complement_subspace)
+  then show ?thesis
+    by (metis closure_translation translation_diff translation_invert)
+qed
+
+corollary dense_complement_openin_affine_hull:
+  fixes S :: "'a :: euclidean_space set"
+  assumes less: "aff_dim T < aff_dim S"
+      and ope: "openin (subtopology euclidean (affine hull S)) S"
+    shows "closure(S - T) = closure S"
+proof -
+  have "affine hull S - T \<subseteq> affine hull S"
+    by blast
+  then have "closure (S \<inter> closure (affine hull S - T)) = closure (S \<inter> (affine hull S - T))"
+    by (rule closure_openin_Int_closure [OF ope])
+  then show ?thesis
+    by (metis Int_Diff aff_dim_affine_hull affine_affine_hull dense_complement_affine hull_subset inf.orderE less)
+qed
+
+corollary dense_complement_convex:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "aff_dim T < aff_dim S" "convex S"
+    shows "closure(S - T) = closure S"
+proof
+  show "closure (S - T) \<subseteq> closure S"
+    by (simp add: Diff_subset closure_mono)
+  have "closure (rel_interior S - T) = closure (rel_interior S)"
+    apply (rule dense_complement_openin_affine_hull)
+    apply (simp add: assms rel_interior_aff_dim)
+    using \<open>convex S\<close> rel_interior_rel_open rel_open by blast
+  then show "closure S \<subseteq> closure (S - T)"
+    by (metis Diff_mono \<open>convex S\<close> closure_mono convex_closure_rel_interior order_refl rel_interior_subset)
+qed
+
+corollary dense_complement_convex_closed:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "aff_dim T < aff_dim S" "convex S" "closed S"
+    shows "closure(S - T) = S"
+  by (simp add: assms dense_complement_convex)
+
+
 subsection\<open>Parallel slices, etc.\<close>
 
 text\<open> If we take a slice out of a set, we can do it perpendicularly,
diff -r c61c957b0439 -r ff2e0115fea4 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Sep 08 11:09:56 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Sep 08 12:49:40 2017 +0100
@@ -2356,6 +2356,28 @@
     done
 qed
 
+lemma closure_openin_Int_closure:
+  assumes ope: "openin (subtopology euclidean U) S" and "T \<subseteq> U"
+  shows "closure(S \<inter> closure T) = closure(S \<inter> T)"
+proof
+  obtain V where "open V" and S: "S = U \<inter> V"
+    using ope using openin_open by metis
+  show "closure (S \<inter> closure T) \<subseteq> closure (S \<inter> T)"
+    proof (clarsimp simp: S)
+      fix x
+      assume  "x \<in> closure (U \<inter> V \<inter> closure T)"
+      then have "V \<inter> closure T \<subseteq> A \<Longrightarrow> x \<in> closure A" for A
+          by (metis closure_mono subsetD inf.coboundedI2 inf_assoc)
+      then have "x \<in> closure (T \<inter> V)"
+         by (metis \<open>open V\<close> closure_closure inf_commute open_Int_closure_subset)
+      then show "x \<in> closure (U \<inter> V \<inter> T)"
+        by (metis \<open>T \<subseteq> U\<close> inf.absorb_iff2 inf_assoc inf_commute)
+    qed
+next
+  show "closure (S \<inter> T) \<subseteq> closure (S \<inter> closure T)"
+    by (meson Int_mono closure_mono closure_subset order_refl)
+qed
+
 lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
   unfolding closure_def using islimpt_punctured by blast
 
@@ -3520,6 +3542,12 @@
   apply (metis dist_self)
   done
 
+lemma closure_approachable_le:
+  fixes S :: "'a::metric_space set"
+  shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x \<le> e)"
+  unfolding closure_approachable
+  using dense by force
+
 lemma closed_approachable:
   fixes S :: "'a::metric_space set"
   shows "closed S \<Longrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
@@ -3544,6 +3572,17 @@
   then show ?thesis unfolding closure_approachable by auto
 qed
 
+lemma closure_Int_ballI:
+  fixes S :: "'a :: metric_space set"
+  assumes "\<And>U. \<lbrakk>openin (subtopology euclidean S) U; U \<noteq> {}\<rbrakk> \<Longrightarrow> T \<inter> U \<noteq> {}"
+ shows "S \<subseteq> closure T"
+proof (clarsimp simp: closure_approachable dist_commute)
+  fix x and e::real
+  assume "x \<in> S" "0 < e"
+  with assms [of "S \<inter> ball x e"] show "\<exists>y\<in>T. dist x y < e"
+    by force
+qed
+
 lemma closed_contains_Inf:
   fixes S :: "real set"
   shows "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> closed S \<Longrightarrow> Inf S \<in> S"
@@ -4802,6 +4841,11 @@
     by (simp add: closure_subset open_Compl)
 qed
 
+corollary closure_Int_ball_not_empty:
+  assumes "S \<subseteq> closure T" "x \<in> S" "r > 0"
+  shows "T \<inter> ball x r \<noteq> {}"
+  using assms centre_in_ball closure_iff_nhds_not_empty by blast
+
 lemma compact_filter:
   "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))"
 proof (intro allI iffI impI compact_fip[THEN iffD2] notI)
@@ -5630,6 +5674,115 @@
     done
 qed
 
+text\<open>The Baire propery of dense sets\<close>
+theorem Baire:
+  fixes S::"'a::{real_normed_vector,heine_borel} set"
+  assumes "closed S" "countable \<G>"
+      and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
+ shows "S \<subseteq> closure(\<Inter>\<G>)"
+proof (cases "\<G> = {}")
+  case True
+  then show ?thesis
+    using closure_subset by auto
+next
+  let ?g = "from_nat_into \<G>"
+  case False
+  then have gin: "?g n \<in> \<G>" for n
+    by (simp add: from_nat_into)
+  show ?thesis
+  proof (clarsimp simp: closure_approachable)
+    fix x and e::real
+    assume "x \<in> S" "0 < e"
+    obtain TF where opeF: "\<And>n. openin (subtopology euclidean S) (TF n)" 
+               and ne: "\<And>n. TF n \<noteq> {}" 
+               and subg: "\<And>n. S \<inter> closure(TF n) \<subseteq> ?g n"
+               and subball: "\<And>n. closure(TF n) \<subseteq> ball x e" 
+               and decr: "\<And>n. TF(Suc n) \<subseteq> TF n"
+    proof -
+      have *: "\<exists>Y. (openin (subtopology euclidean S) Y \<and> Y \<noteq> {} \<and>
+                   S \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> U" 
+        if opeU: "openin (subtopology euclidean S) U" and "U \<noteq> {}" and cloU: "closure U \<subseteq> ball x e" for U n
+      proof -
+        obtain T where T: "open T" "U = T \<inter> S"
+          using \<open>openin (subtopology euclidean S) U\<close> by (auto simp: openin_subtopology)
+        with \<open>U \<noteq> {}\<close> have "T \<inter> closure (?g n) \<noteq> {}"
+          using gin ope by fastforce
+        then have "T \<inter> ?g n \<noteq> {}"
+          using \<open>open T\<close> open_Int_closure_eq_empty by blast
+        then obtain y where "y \<in> U" "y \<in> ?g n"
+          using T ope [of "?g n", OF gin] by (blast dest:  openin_imp_subset)
+        moreover have "openin (subtopology euclidean S) (U \<inter> ?g n)"
+          using gin ope opeU by blast
+        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"
+          by (force simp add: openin_contains_ball)
+        show ?thesis
+        proof (intro exI conjI)
+          show "openin (subtopology euclidean S) (S \<inter> ball y (d/2))"
+            by (simp add: openin_open_Int)
+          show "S \<inter> ball y (d/2) \<noteq> {}"
+            using \<open>0 < d\<close> \<open>y \<in> U\<close> opeU openin_imp_subset by fastforce
+          have "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> closure (ball y (d/2))"
+            using closure_mono by blast
+          also have "... \<subseteq> ?g n"
+            using \<open>d > 0\<close> d by force
+          finally show "S \<inter> closure (S \<inter> ball y (d/2)) \<subseteq> ?g n" .
+          have "closure (S \<inter> ball y (d/2)) \<subseteq> S \<inter> ball y d"
+          proof -
+            have "closure (ball y (d/2)) \<subseteq> ball y d"
+              using \<open>d > 0\<close> by auto
+            then have "closure (S \<inter> ball y (d/2)) \<subseteq> ball y d"
+              by (meson closure_mono inf.cobounded2 subset_trans)
+            then show ?thesis
+              by (simp add: \<open>closed S\<close> closure_minimal)
+          qed
+          also have "...  \<subseteq> ball x e"
+            using cloU closure_subset d by blast
+          finally show "closure (S \<inter> ball y (d/2)) \<subseteq> ball x e" .
+          show "S \<inter> ball y (d/2) \<subseteq> U"
+            using ball_divide_subset_numeral d by blast
+        qed
+      qed
+      let ?\<Phi> = "\<lambda>n X. openin (subtopology euclidean S) X \<and> X \<noteq> {} \<and> 
+                      S \<inter> closure X \<subseteq> ?g n \<and> closure X \<subseteq> ball x e"
+      have "closure (S \<inter> ball x (e / 2)) \<subseteq> closure(ball x (e/2))"
+        by (simp add: closure_mono)
+      also have "...  \<subseteq> ball x e"
+        using \<open>e > 0\<close> by auto
+      finally have "closure (S \<inter> ball x (e / 2)) \<subseteq> ball x e" .
+      moreover have"openin (subtopology euclidean S) (S \<inter> ball x (e / 2))" "S \<inter> ball x (e / 2) \<noteq> {}"
+        using \<open>0 < e\<close> \<open>x \<in> S\<close> by auto
+      ultimately obtain Y where Y: "?\<Phi> 0 Y \<and> Y \<subseteq> S \<inter> ball x (e / 2)"
+            using * [of "S \<inter> ball x (e/2)" 0] by metis
+      show thesis
+      proof (rule exE [OF dependent_nat_choice [of ?\<Phi> "\<lambda>n X Y. Y \<subseteq> X"]])
+        show "\<exists>x. ?\<Phi> 0 x"
+          using Y by auto
+        show "\<exists>Y. ?\<Phi> (Suc n) Y \<and> Y \<subseteq> X" if "?\<Phi> n X" for X n
+          using that by (blast intro: *)
+      qed (use that in metis)
+    qed
+    have "(\<Inter>n. S \<inter> closure (TF n)) \<noteq> {}"
+    proof (rule compact_nest)
+      show "\<And>n. compact (S \<inter> closure (TF n))"
+        by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF \<open>closed S\<close>])
+      show "\<And>n. S \<inter> closure (TF n) \<noteq> {}" 
+        by (metis Int_absorb1 opeF \<open>closed S\<close> closure_eq_empty closure_minimal ne openin_imp_subset)
+      show "\<And>m n. m \<le> n \<Longrightarrow> S \<inter> closure (TF n) \<subseteq> S \<inter> closure (TF m)"
+        by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le)
+    qed
+    moreover have "(\<Inter>n. S \<inter> closure (TF n)) \<subseteq> {y \<in> \<Inter>\<G>. dist y x < e}"
+    proof (clarsimp, intro conjI)
+      fix y
+      assume "y \<in> S" and y: "\<forall>n. y \<in> closure (TF n)"
+      then show "\<forall>T\<in>\<G>. y \<in> T"
+        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] set_mp subg)
+      show "dist y x < e"
+        by (metis y dist_commute mem_ball subball subsetCE)
+    qed
+    ultimately show "\<exists>y \<in> \<Inter>\<G>. dist y x < e"
+      by auto
+  qed
+qed
 
 subsubsection \<open>Completeness\<close>