--- 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:
--- 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"
--- 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:
--- 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
--- 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,
--- 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>