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