--- a/src/HOL/Analysis/Borel_Space.thy Mon Jan 28 20:32:09 2019 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy Mon Jan 28 18:36:50 2019 -0500
@@ -576,9 +576,9 @@
shows "borel = sigma UNIV B"
unfolding borel_def
proof (intro sigma_eqI sigma_sets_eqI, safe)
- interpret countable_basis using assms by unfold_locales
+ interpret countable_basis "open" B using assms by (rule countable_basis_openI)
fix X::"'a set" assume "open X"
- from open_countable_basisE[OF this] guess B' . note B' = this
+ from open_countable_basisE[OF this] obtain B' where B': "B' \<subseteq> B" "X = \<Union> B'" .
then show "X \<in> sigma_sets UNIV B"
by (blast intro: sigma_sets_UNION \<open>countable B\<close> countable_subset)
next
--- a/src/HOL/Analysis/Elementary_Topology.thy Mon Jan 28 20:32:09 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Mon Jan 28 18:36:50 2019 -0500
@@ -270,26 +270,26 @@
subsection \<open>Countable Basis\<close>
-locale%important countable_basis =
- fixes B :: "'a::topological_space set set"
+locale%important countable_basis = topological_space p for p::"'a set \<Rightarrow> bool" +
+ fixes B :: "'a set set"
assumes is_basis: "topological_basis B"
and countable_basis: "countable B"
begin
lemma open_countable_basis_ex:
- assumes "open X"
+ assumes "p X"
shows "\<exists>B' \<subseteq> B. X = \<Union>B'"
using assms countable_basis is_basis
unfolding topological_basis_def by blast
lemma open_countable_basisE:
- assumes "open X"
+ assumes "p X"
obtains B' where "B' \<subseteq> B" "X = \<Union>B'"
using assms open_countable_basis_ex
by atomize_elim simp
lemma countable_dense_exists:
- "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
+ "\<exists>D::'a set. countable D \<and> (\<forall>X. p X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
proof -
let ?f = "(\<lambda>B'. SOME x. x \<in> B')"
have "countable (?f ` B)" using countable_basis by simp
@@ -299,11 +299,17 @@
lemma countable_dense_setE:
obtains D :: "'a set"
- where "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X"
+ where "countable D" "\<And>X. p X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X"
using countable_dense_exists by blast
end
+lemma countable_basis_openI: "countable_basis open B"
+ if "countable B" "topological_basis B"
+ using that
+ by unfold_locales
+ (simp_all add: topological_basis topological_space.topological_basis topological_space_axioms)
+
lemma (in first_countable_topology) first_countable_basisE:
fixes x :: 'a
obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
@@ -415,7 +421,7 @@
class second_countable_topology = topological_space +
assumes ex_countable_subbasis:
- "\<exists>B::'a::topological_space set set. countable B \<and> open = generate_topology B"
+ "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
begin
lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B"
@@ -460,8 +466,8 @@
then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)"
unfolding subset_image_iff by blast }
then show "topological_basis ?B"
- unfolding topological_space_class.topological_basis_def
- by (safe intro!: topological_space_class.open_Inter)
+ unfolding topological_basis_def
+ by (safe intro!: open_Inter)
(simp_all add: B generate_topology.Basis subset_eq)
qed
qed
@@ -520,7 +526,7 @@
qed
sublocale second_countable_topology <
- countable_basis "SOME B. countable B \<and> topological_basis B"
+ countable_basis "open" "SOME B. countable B \<and> topological_basis B"
using someI_ex[OF ex_countable_basis]
by unfold_locales safe