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
```