src/HOL/Analysis/Connected.thy
 changeset 68607 67bb59e49834 parent 68527 2f4e2aab190a child 69064 5840724b1d71
```     1.1 --- a/src/HOL/Analysis/Connected.thy	Mon Jul 09 21:55:40 2018 +0100
1.2 +++ b/src/HOL/Analysis/Connected.thy	Tue Jul 10 09:38:35 2018 +0200
1.3 @@ -776,12 +776,12 @@
1.4
1.5  subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
1.6
1.7 -proposition%important bounded_closed_chain:
1.8 +proposition bounded_closed_chain:
1.9    fixes \<F> :: "'a::heine_borel set set"
1.10    assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
1.11        and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
1.12      shows "\<Inter>\<F> \<noteq> {}"
1.13 -proof%unimportant -
1.14 +proof -
1.15    have "B \<inter> \<Inter>\<F> \<noteq> {}"
1.16    proof (rule compact_imp_fip)
1.17      show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
1.18 @@ -824,12 +824,12 @@
1.19    then show ?thesis by blast
1.20  qed
1.21
1.22 -corollary%important compact_chain:
1.23 +corollary compact_chain:
1.24    fixes \<F> :: "'a::heine_borel set set"
1.25    assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
1.26            "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
1.27      shows "\<Inter> \<F> \<noteq> {}"
1.28 -proof%unimportant (cases "\<F> = {}")
1.29 +proof (cases "\<F> = {}")
1.30    case True
1.31    then show ?thesis by auto
1.32  next
1.33 @@ -852,12 +852,12 @@
1.34  qed
1.35
1.36  text\<open>The Baire property of dense sets\<close>
1.37 -theorem%important Baire:
1.38 +theorem Baire:
1.39    fixes S::"'a::{real_normed_vector,heine_borel} set"
1.40    assumes "closed S" "countable \<G>"
1.41        and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
1.42   shows "S \<subseteq> closure(\<Inter>\<G>)"
1.43 -proof%unimportant (cases "\<G> = {}")
1.44 +proof (cases "\<G> = {}")
1.45    case True
1.46    then show ?thesis
1.47      using closure_subset by auto
1.48 @@ -2443,11 +2443,11 @@
1.49    ultimately show ?thesis using that by blast
1.50  qed
1.51
1.52 -corollary%important compact_uniformly_continuous:
1.53 +corollary compact_uniformly_continuous:
1.54    fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
1.55    assumes f: "continuous_on S f" and S: "compact S"
1.56    shows "uniformly_continuous_on S f"
1.57 -  using%unimportant f
1.58 +  using f
1.59      unfolding continuous_on_iff uniformly_continuous_on_def
1.60      by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])
1.61
1.62 @@ -2929,11 +2929,11 @@
1.63
1.64  subsection \<open>Separation between points and sets\<close>
1.65
1.66 -lemma%important separate_point_closed:
1.67 +proposition separate_point_closed:
1.68    fixes s :: "'a::heine_borel set"
1.69    assumes "closed s" and "a \<notin> s"
1.70    shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"
1.71 -proof%unimportant (cases "s = {}")
1.72 +proof (cases "s = {}")
1.73    case True
1.74    then show ?thesis by(auto intro!: exI[where x=1])
1.75  next
1.76 @@ -2944,12 +2944,12 @@
1.77      by blast
1.78  qed
1.79
1.80 -lemma%important separate_compact_closed:
1.81 +proposition separate_compact_closed:
1.82    fixes s t :: "'a::heine_borel set"
1.83    assumes "compact s"
1.84      and t: "closed t" "s \<inter> t = {}"
1.85    shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
1.86 -proof%unimportant cases
1.87 +proof cases
1.88    assume "s \<noteq> {} \<and> t \<noteq> {}"
1.89    then have "s \<noteq> {}" "t \<noteq> {}" by auto
1.90    let ?inf = "\<lambda>x. infdist x t"
1.91 @@ -2964,27 +2964,27 @@
1.92    ultimately show ?thesis by auto
1.93  qed (auto intro!: exI[of _ 1])
1.94
1.95 -lemma%important separate_closed_compact:
1.96 +proposition separate_closed_compact:
1.97    fixes s t :: "'a::heine_borel set"
1.98    assumes "closed s"
1.99      and "compact t"
1.100      and "s \<inter> t = {}"
1.101    shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
1.102 -proof%unimportant -
1.103 +proof -
1.104    have *: "t \<inter> s = {}"
1.105      using assms(3) by auto
1.106    show ?thesis
1.107      using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
1.108  qed
1.109
1.110 -lemma%important compact_in_open_separated:
1.111 +proposition compact_in_open_separated:
1.112    fixes A::"'a::heine_borel set"
1.113    assumes "A \<noteq> {}"
1.114    assumes "compact A"
1.115    assumes "open B"
1.116    assumes "A \<subseteq> B"
1.117    obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
1.118 -proof%unimportant atomize_elim
1.119 +proof atomize_elim
1.120    have "closed (- B)" "compact A" "- B \<inter> A = {}"
1.121      using assms by (auto simp: open_Diff compact_eq_bounded_closed)
1.122    from separate_closed_compact[OF this]
1.123 @@ -3959,12 +3959,12 @@
1.124      unfolding complete_def by auto
1.125  qed
1.126
1.127 -lemma%important injective_imp_isometric:
1.128 +proposition injective_imp_isometric:
1.129    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.130    assumes s: "closed s" "subspace s"
1.131      and f: "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0"
1.132    shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm x"
1.133 -proof%unimportant (cases "s \<subseteq> {0::'a}")
1.134 +proof (cases "s \<subseteq> {0::'a}")
1.135    case True
1.136    have "norm x \<le> norm (f x)" if "x \<in> s" for x
1.137    proof -
1.138 @@ -4032,11 +4032,11 @@
1.139    ultimately show ?thesis by auto
1.140  qed
1.141
1.142 -lemma%important closed_injective_image_subspace:
1.143 +proposition closed_injective_image_subspace:
1.144    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.145    assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0" "closed s"
1.146    shows "closed(f ` s)"
1.147 -proof%unimportant -
1.148 +proof -
1.149    obtain e where "e > 0" and e: "\<forall>x\<in>s. e * norm x \<le> norm (f x)"
1.150      using injective_imp_isometric[OF assms(4,1,2,3)] by auto
1.151    show ?thesis
1.152 @@ -4182,13 +4182,13 @@
1.153
1.154  subsection \<open>Banach fixed point theorem (not really topological ...)\<close>
1.155
1.156 -theorem%important banach_fix:
1.157 +theorem banach_fix:
1.158    assumes s: "complete s" "s \<noteq> {}"
1.159      and c: "0 \<le> c" "c < 1"
1.160      and f: "f ` s \<subseteq> s"
1.161      and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
1.162    shows "\<exists>!x\<in>s. f x = x"
1.163 -proof%unimportant -
1.164 +proof -
1.165    from c have "1 - c > 0" by simp
1.166
1.167    from s(2) obtain z0 where z0: "z0 \<in> s" by blast
1.168 @@ -4338,13 +4338,13 @@
1.169
1.170  subsection \<open>Edelstein fixed point theorem\<close>
1.171
1.172 -theorem%important edelstein_fix:
1.173 +theorem edelstein_fix:
1.174    fixes s :: "'a::metric_space set"
1.175    assumes s: "compact s" "s \<noteq> {}"
1.176      and gs: "(g ` s) \<subseteq> s"
1.177      and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
1.178    shows "\<exists>!x\<in>s. g x = x"
1.179 -proof%unimportant -
1.180 +proof -
1.181    let ?D = "(\<lambda>x. (x, x)) ` s"
1.182    have D: "compact ?D" "?D \<noteq> {}"
1.183      by (rule compact_continuous_image)
1.184 @@ -4693,10 +4693,10 @@
1.185      done
1.186  qed
1.187
1.188 -proposition%important separable:
1.189 +proposition separable:
1.190    fixes S :: "'a:: euclidean_space set"
1.191    obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
1.192 -proof%unimportant -
1.193 +proof -
1.194    obtain \<B> :: "'a:: euclidean_space set set"
1.195      where "countable \<B>"
1.196        and "{} \<notin> \<B>"
1.197 @@ -4739,11 +4739,11 @@
1.198    qed
1.199  qed
1.200
1.201 -proposition%important Lindelof:
1.202 +proposition Lindelof:
1.203    fixes \<F> :: "'a::euclidean_space set set"
1.204    assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
1.205    obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
1.206 -proof%unimportant -
1.207 +proof -
1.208    obtain \<B> :: "'a set set"
1.209      where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
1.210        and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
1.211 @@ -5045,11 +5045,11 @@
1.212  qed
1.213
1.214
1.215 -proposition%important component_diff_connected:
1.216 +proposition component_diff_connected:
1.217    fixes S :: "'a::metric_space set"
1.218    assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
1.219    shows "connected(U - C)"
1.220 -  using%unimportant \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
1.221 +  using \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
1.222  proof clarify
1.223    fix H3 H4
1.224    assume clo3: "closedin (subtopology euclidean (U - C)) H3"
1.225 @@ -5175,11 +5175,11 @@
1.226      by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
1.227  qed
1.228
1.229 -proposition%important tendsto_componentwise_iff:
1.230 +proposition tendsto_componentwise_iff:
1.231    fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
1.232    shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
1.233           (is "?lhs = ?rhs")
1.234 -proof%unimportant
1.235 +proof
1.236    assume ?lhs
1.237    then show ?rhs
1.238      unfolding tendsto_def
```