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.4  
     1.5  text{*Compactness expressed with filters*}
     1.6  
     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.79  
    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)