src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 57276 49c51eeaa623 parent 57275 0ddb5b755cdc child 57418 6ab1c7cb0b8d
1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 18 07:31:12 2014 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 18 14:31:32 2014 +0200
1.3 @@ -3262,38 +3262,6 @@
1.5  text{*Compactness expressed with filters*}
1.7 -definition "filter_from_subbase B = Abs_filter (\<lambda>P. \<exists>X \<subseteq> B. finite X \<and> Inf X \<le> P)"
1.8 -
1.9 -lemma eventually_filter_from_subbase:
1.10 -  "eventually P (filter_from_subbase B) \<longleftrightarrow> (\<exists>X \<subseteq> B. finite X \<and> Inf X \<le> P)"
1.11 -    (is "_ \<longleftrightarrow> ?R P")
1.12 -  unfolding filter_from_subbase_def
1.13 -proof (rule eventually_Abs_filter is_filter.intro)+
1.14 -  show "?R (\<lambda>x. True)"
1.15 -    by (rule exI[of _ "{}"]) (simp add: le_fun_def)
1.16 -next
1.17 -  fix P Q
1.18 -  assume "?R P" then guess X ..
1.19 -  moreover
1.20 -  assume "?R Q" then guess Y ..
1.21 -  ultimately show "?R (\<lambda>x. P x \<and> Q x)"
1.22 -    by (intro exI[of _ "X \<union> Y"]) auto
1.23 -next
1.24 -  fix P Q
1.25 -  assume "?R P" then guess X ..
1.26 -  moreover assume "\<forall>x. P x \<longrightarrow> Q x"
1.27 -  ultimately show "?R Q"
1.28 -    by (intro exI[of _ X]) auto
1.29 -qed
1.30 -
1.31 -lemma eventually_filter_from_subbaseI: "P \<in> B \<Longrightarrow> eventually P (filter_from_subbase B)"
1.32 -  by (subst eventually_filter_from_subbase) (auto intro!: exI[of _ "{P}"])
1.33 -
1.34 -lemma filter_from_subbase_not_bot:
1.35 -  "\<forall>X \<subseteq> B. finite X \<longrightarrow> Inf X \<noteq> bot \<Longrightarrow> filter_from_subbase B \<noteq> bot"
1.36 -  unfolding trivial_limit_def eventually_filter_from_subbase
1.37 -    bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp
1.38 -
1.39  lemma closure_iff_nhds_not_empty:
1.40    "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})"
1.41  proof safe
1.42 @@ -3360,34 +3328,31 @@
1.43  next
1.44    fix A
1.45    assume A: "\<forall>a\<in>A. closed a" "\<forall>B\<subseteq>A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}" "U \<inter> \<Inter>A = {}"
1.46 -  def P' \<equiv> "(\<lambda>a (x::'a). x \<in> a)"
1.47 -  then have inj_P': "\<And>A. inj_on P' A"
1.48 -    by (auto intro!: inj_onI simp: fun_eq_iff)
1.49 -  def F \<equiv> "filter_from_subbase (P' ` insert U A)"
1.50 +  def F \<equiv> "INF a:insert U A. principal a"
1.51    have "F \<noteq> bot"
1.52      unfolding F_def
1.53 -  proof (safe intro!: filter_from_subbase_not_bot)
1.54 -    fix X
1.55 -    assume "X \<subseteq> P' ` insert U A" "finite X" "Inf X = bot"
1.56 -    then obtain B where "B \<subseteq> insert U A" "finite B" and B: "Inf (P' ` B) = bot"
1.57 -      unfolding subset_image_iff by (auto intro: inj_P' finite_imageD simp del: Inf_image_eq)
1.58 -    with A(2)[THEN spec, of "B - {U}"] have "U \<inter> \<Inter>(B - {U}) \<noteq> {}"
1.59 +  proof (rule INF_filter_not_bot)
1.60 +    fix X assume "X \<subseteq> insert U A" "finite X"
1.61 +    moreover with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
1.62        by auto
1.63 -    with B show False
1.64 -      by (auto simp: P'_def fun_eq_iff)
1.65 +    ultimately show "(INF a:X. principal a) \<noteq> bot"
1.66 +      by (auto simp add: INF_principal_finite principal_eq_bot_iff)
1.67    qed
1.68 -  moreover have "eventually (\<lambda>x. x \<in> U) F"
1.69 -    unfolding F_def by (rule eventually_filter_from_subbaseI) (auto simp: P'_def)
1.70 +  moreover
1.71 +  have "F \<le> principal U"
1.72 +    unfolding F_def by auto
1.73 +  then have "eventually (\<lambda>x. x \<in> U) F"
1.74 +    by (auto simp: le_filter_def eventually_principal)
1.75    moreover
1.76    assume "\<forall>F. F \<noteq> bot \<longrightarrow> eventually (\<lambda>x. x \<in> U) F \<longrightarrow> (\<exists>x\<in>U. inf (nhds x) F \<noteq> bot)"
1.77    ultimately obtain x where "x \<in> U" and x: "inf (nhds x) F \<noteq> bot"
1.78      by auto
1.80 -  {
1.81 -    fix V
1.82 -    assume "V \<in> A"
1.83 +  { fix V assume "V \<in> A"
1.84 +    then have "F \<le> principal V"
1.85 +      unfolding F_def by (intro INF_lower2[of V]) auto
1.86      then have V: "eventually (\<lambda>x. x \<in> V) F"
1.87 -      by (auto simp add: F_def image_iff P'_def intro!: eventually_filter_from_subbaseI)
1.88 +      by (auto simp: le_filter_def eventually_principal)
1.89      have "x \<in> closure V"
1.90        unfolding closure_iff_nhds_not_empty
1.91      proof (intro impI allI)