src/HOL/Analysis/Topology_Euclidean_Space.thy
changeset 68607 67bb59e49834
parent 68532 f8b98d31ad45
child 68617 75129a73aca3
     1.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jul 09 21:55:40 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jul 10 09:38:35 2018 +0200
     1.3 @@ -640,7 +640,7 @@
     1.4  
     1.5  subsubsection \<open>Main properties of open sets\<close>
     1.6  
     1.7 -lemma%important openin_clauses:
     1.8 +proposition openin_clauses:
     1.9    fixes U :: "'a topology"
    1.10    shows
    1.11      "openin U {}"
    1.12 @@ -2765,16 +2765,16 @@
    1.13  
    1.14  subsection \<open>Limits\<close>
    1.15  
    1.16 -lemma%important Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
    1.17 +proposition Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
    1.18    by (auto simp: tendsto_iff trivial_limit_eq)
    1.19  
    1.20  text \<open>Show that they yield usual definitions in the various cases.\<close>
    1.21  
    1.22 -lemma%important Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
    1.23 +proposition Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
    1.24      (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)"
    1.25    by (auto simp: tendsto_iff eventually_at_le)
    1.26  
    1.27 -lemma%important Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
    1.28 +proposition Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
    1.29      (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a  < d \<longrightarrow> dist (f x) l < e)"
    1.30    by (auto simp: tendsto_iff eventually_at)
    1.31  
    1.32 @@ -2785,11 +2785,11 @@
    1.33    apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
    1.34    done
    1.35  
    1.36 -lemma%important Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
    1.37 +proposition Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
    1.38      (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
    1.39    by (auto simp: tendsto_iff eventually_at)
    1.40  
    1.41 -lemma%important Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
    1.42 +proposition Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
    1.43    by (auto simp: tendsto_iff eventually_at_infinity)
    1.44  
    1.45  corollary Lim_at_infinityI [intro?]:
    1.46 @@ -3652,12 +3652,12 @@
    1.47  
    1.48  subsubsection \<open>Bolzano-Weierstrass property\<close>
    1.49  
    1.50 -lemma%important heine_borel_imp_bolzano_weierstrass:
    1.51 +proposition heine_borel_imp_bolzano_weierstrass:
    1.52    assumes "compact s"
    1.53      and "infinite t"
    1.54      and "t \<subseteq> s"
    1.55    shows "\<exists>x \<in> s. x islimpt t"
    1.56 -proof%unimportant (rule ccontr)
    1.57 +proof (rule ccontr)
    1.58    assume "\<not> (\<exists>x \<in> s. x islimpt t)"
    1.59    then obtain f where f: "\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)"
    1.60      unfolding islimpt_def
    1.61 @@ -4170,9 +4170,9 @@
    1.62      unfolding C_def by (intro exI[of _ "f`T"]) fastforce
    1.63  qed
    1.64  
    1.65 -lemma%important countably_compact_imp_compact_second_countable:
    1.66 +proposition countably_compact_imp_compact_second_countable:
    1.67    "countably_compact U \<Longrightarrow> compact (U :: 'a :: second_countable_topology set)"
    1.68 -proof%unimportant (rule countably_compact_imp_compact)
    1.69 +proof (rule countably_compact_imp_compact)
    1.70    fix T and x :: 'a
    1.71    assume "open T" "x \<in> T"
    1.72    from topological_basisE[OF is_basis this] obtain b where
    1.73 @@ -4448,10 +4448,10 @@
    1.74    shows "seq_compact U \<longleftrightarrow> compact U"
    1.75    using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
    1.76  
    1.77 -lemma%important bolzano_weierstrass_imp_seq_compact:
    1.78 +proposition bolzano_weierstrass_imp_seq_compact:
    1.79    fixes s :: "'a::{t1_space, first_countable_topology} set"
    1.80    shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
    1.81 -  by%unimportant (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
    1.82 +  by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
    1.83  
    1.84  
    1.85  subsubsection\<open>Totally bounded\<close>
    1.86 @@ -4459,10 +4459,10 @@
    1.87  lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (s m) (s n) < e)"
    1.88    unfolding Cauchy_def by metis
    1.89  
    1.90 -lemma%important seq_compact_imp_totally_bounded:
    1.91 +proposition seq_compact_imp_totally_bounded:
    1.92    assumes "seq_compact s"
    1.93    shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
    1.94 -proof%unimportant -
    1.95 +proof -
    1.96    { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"
    1.97      let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
    1.98      have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
    1.99 @@ -4491,11 +4491,11 @@
   1.100  
   1.101  subsubsection\<open>Heine-Borel theorem\<close>
   1.102  
   1.103 -lemma%important seq_compact_imp_heine_borel:
   1.104 +proposition seq_compact_imp_heine_borel:
   1.105    fixes s :: "'a :: metric_space set"
   1.106    assumes "seq_compact s"
   1.107    shows "compact s"
   1.108 -proof%unimportant -
   1.109 +proof -
   1.110    from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>]
   1.111    obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)"
   1.112      unfolding choice_iff' ..
   1.113 @@ -4536,22 +4536,22 @@
   1.114    qed
   1.115  qed
   1.116  
   1.117 -lemma%important compact_eq_seq_compact_metric:
   1.118 +proposition compact_eq_seq_compact_metric:
   1.119    "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
   1.120    using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
   1.121  
   1.122 -lemma%important compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
   1.123 +proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
   1.124    "compact (S :: 'a::metric_space set) \<longleftrightarrow>
   1.125     (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
   1.126    unfolding compact_eq_seq_compact_metric seq_compact_def by auto
   1.127  
   1.128  subsubsection \<open>Complete the chain of compactness variants\<close>
   1.129  
   1.130 -lemma%important compact_eq_bolzano_weierstrass:
   1.131 +proposition compact_eq_bolzano_weierstrass:
   1.132    fixes s :: "'a::metric_space set"
   1.133    shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"
   1.134    (is "?lhs = ?rhs")
   1.135 -proof%unimportant
   1.136 +proof
   1.137    assume ?lhs
   1.138    then show ?rhs
   1.139      using heine_borel_imp_bolzano_weierstrass[of s] by auto
   1.140 @@ -4561,7 +4561,7 @@
   1.141      unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
   1.142  qed
   1.143  
   1.144 -lemma%important bolzano_weierstrass_imp_bounded:
   1.145 +proposition bolzano_weierstrass_imp_bounded:
   1.146    "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
   1.147    using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
   1.148  
   1.149 @@ -4577,12 +4577,12 @@
   1.150    assumes bounded_imp_convergent_subsequence:
   1.151      "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
   1.152  
   1.153 -lemma%important bounded_closed_imp_seq_compact:
   1.154 +proposition bounded_closed_imp_seq_compact:
   1.155    fixes s::"'a::heine_borel set"
   1.156    assumes "bounded s"
   1.157      and "closed s"
   1.158    shows "seq_compact s"
   1.159 -proof%unimportant (unfold seq_compact_def, clarify)
   1.160 +proof (unfold seq_compact_def, clarify)
   1.161    fix f :: "nat \<Rightarrow> 'a"
   1.162    assume f: "\<forall>n. f n \<in> s"
   1.163    with \<open>bounded s\<close> have "bounded (range f)"
   1.164 @@ -4807,12 +4807,12 @@
   1.165  
   1.166  subsubsection \<open>Completeness\<close>
   1.167  
   1.168 -lemma%important (in metric_space) completeI:
   1.169 +proposition (in metric_space) completeI:
   1.170    assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
   1.171    shows "complete s"
   1.172    using assms unfolding complete_def by fast
   1.173  
   1.174 -lemma%important (in metric_space) completeE:
   1.175 +proposition (in metric_space) completeE:
   1.176    assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
   1.177    obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
   1.178    using assms unfolding complete_def by fast
   1.179 @@ -4862,10 +4862,10 @@
   1.180    then show ?thesis unfolding complete_def by auto
   1.181  qed
   1.182  
   1.183 -lemma%important compact_eq_totally_bounded:
   1.184 +proposition compact_eq_totally_bounded:
   1.185    "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
   1.186      (is "_ \<longleftrightarrow> ?rhs")
   1.187 -proof%unimportant
   1.188 +proof
   1.189    assume assms: "?rhs"
   1.190    then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)"
   1.191      by (auto simp: choice_iff')
   1.192 @@ -5069,7 +5069,7 @@
   1.193  
   1.194  text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
   1.195  
   1.196 -lemma%important continuous_within_eps_delta:
   1.197 +proposition continuous_within_eps_delta:
   1.198    "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"
   1.199    unfolding continuous_within and Lim_within  by fastforce
   1.200