src/HOL/Analysis/Starlike.thy
changeset 68607 67bb59e49834
parent 68527 2f4e2aab190a
child 68796 9ca183045102
     1.1 --- a/src/HOL/Analysis/Starlike.thy	Mon Jul 09 21:55:40 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Starlike.thy	Tue Jul 10 09:38:35 2018 +0200
     1.3 @@ -5063,12 +5063,12 @@
     1.4  
     1.5  subsection\<open>Connectedness of the intersection of a chain\<close>
     1.6  
     1.7 -proposition%important connected_chain:
     1.8 +proposition connected_chain:
     1.9    fixes \<F> :: "'a :: euclidean_space set set"
    1.10    assumes cc: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S \<and> connected S"
    1.11        and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
    1.12    shows "connected(\<Inter>\<F>)"
    1.13 -proof%unimportant (cases "\<F> = {}")
    1.14 +proof (cases "\<F> = {}")
    1.15    case True then show ?thesis
    1.16      by auto
    1.17  next
    1.18 @@ -5212,13 +5212,13 @@
    1.19        by (meson le_max_iff_disj)
    1.20  qed
    1.21  
    1.22 -proposition%important proper_map:
    1.23 +proposition proper_map:
    1.24    fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
    1.25    assumes "closedin (subtopology euclidean S) K"
    1.26        and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact (S \<inter> f -` U)"
    1.27        and "f ` S \<subseteq> T"
    1.28      shows "closedin (subtopology euclidean T) (f ` K)"
    1.29 -proof%unimportant -
    1.30 +proof -
    1.31    have "K \<subseteq> S"
    1.32      using assms closedin_imp_subset by metis
    1.33    obtain C where "closed C" and Keq: "K = S \<inter> C"
    1.34 @@ -6708,11 +6708,11 @@
    1.35    by (metis a orthogonal_clauses(1,2,4)
    1.36        span_induct_alt x)
    1.37  
    1.38 -proposition%important Gram_Schmidt_step:
    1.39 +proposition Gram_Schmidt_step:
    1.40    fixes S :: "'a::euclidean_space set"
    1.41    assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
    1.42      shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
    1.43 -proof%unimportant -
    1.44 +proof -
    1.45    have "finite S"
    1.46      by (simp add: S pairwise_orthogonal_imp_finite)
    1.47    have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
    1.48 @@ -6767,11 +6767,11 @@
    1.49  qed
    1.50  
    1.51  
    1.52 -proposition%important orthogonal_extension:
    1.53 +proposition orthogonal_extension:
    1.54    fixes S :: "'a::euclidean_space set"
    1.55    assumes S: "pairwise orthogonal S"
    1.56    obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
    1.57 -proof%unimportant -
    1.58 +proof -
    1.59    obtain B where "finite B" "span B = span T"
    1.60      using basis_subspace_exists [of "span T"] subspace_span by metis
    1.61    with orthogonal_extension_aux [of B S]
    1.62 @@ -6827,13 +6827,13 @@
    1.63      done
    1.64  qed
    1.65  
    1.66 -proposition%important orthonormal_basis_subspace:
    1.67 +proposition orthonormal_basis_subspace:
    1.68    fixes S :: "'a :: euclidean_space set"
    1.69    assumes "subspace S"
    1.70    obtains B where "B \<subseteq> S" "pairwise orthogonal B"
    1.71                and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
    1.72                and "independent B" "card B = dim S" "span B = S"
    1.73 -proof%unimportant -
    1.74 +proof -
    1.75    obtain B where "0 \<notin> B" "B \<subseteq> S"
    1.76               and orth: "pairwise orthogonal B"
    1.77               and "independent B" "card B = dim S" "span B = S"
    1.78 @@ -6864,11 +6864,11 @@
    1.79  qed
    1.80  
    1.81  
    1.82 -proposition%important orthogonal_to_subspace_exists_gen:
    1.83 +proposition orthogonal_to_subspace_exists_gen:
    1.84    fixes S :: "'a :: euclidean_space set"
    1.85    assumes "span S \<subset> span T"
    1.86    obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
    1.87 -proof%unimportant -
    1.88 +proof -
    1.89    obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
    1.90               and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
    1.91               and "independent B" "card B = dim S" "span B = span S"
    1.92 @@ -6933,10 +6933,10 @@
    1.93      by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
    1.94  qed
    1.95  
    1.96 -proposition%important orthogonal_subspace_decomp_exists:
    1.97 +proposition orthogonal_subspace_decomp_exists:
    1.98    fixes S :: "'a :: euclidean_space set"
    1.99    obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
   1.100 -proof%unimportant -
   1.101 +proof -
   1.102    obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T"
   1.103      "card T = dim (span S)" "span T = span S"
   1.104      using orthogonal_basis_subspace subspace_span by blast
   1.105 @@ -7030,11 +7030,11 @@
   1.106    qed
   1.107  qed
   1.108  
   1.109 -proposition%important dim_orthogonal_sum:
   1.110 +proposition dim_orthogonal_sum:
   1.111    fixes A :: "'a::euclidean_space set"
   1.112    assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.113      shows "dim(A \<union> B) = dim A + dim B"
   1.114 -proof%unimportant -
   1.115 +proof -
   1.116    have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.117      by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
   1.118    have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
   1.119 @@ -7163,10 +7163,10 @@
   1.120  
   1.121  subsection\<open>Lower-dimensional affine subsets are nowhere dense\<close>
   1.122  
   1.123 -proposition%important dense_complement_subspace:
   1.124 +proposition dense_complement_subspace:
   1.125    fixes S :: "'a :: euclidean_space set"
   1.126    assumes dim_less: "dim T < dim S" and "subspace S" shows "closure(S - T) = S"
   1.127 -proof%unimportant -
   1.128 +proof -
   1.129    have "closure(S - U) = S" if "dim U < dim S" "U \<subseteq> S" for U
   1.130    proof -
   1.131      have "span U \<subset> span S"
   1.132 @@ -7465,7 +7465,7 @@
   1.133  
   1.134  subsection\<open>Several Variants of Paracompactness\<close>
   1.135  
   1.136 -proposition%important paracompact:
   1.137 +proposition paracompact:
   1.138    fixes S :: "'a :: euclidean_space set"
   1.139    assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
   1.140    obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
   1.141 @@ -7473,7 +7473,7 @@
   1.142                 and "\<And>x. x \<in> S
   1.143                         \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
   1.144                                 finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
   1.145 -proof%unimportant (cases "S = {}")
   1.146 +proof (cases "S = {}")
   1.147    case True with that show ?thesis by blast
   1.148  next
   1.149    case False
   1.150 @@ -7858,14 +7858,14 @@
   1.151  
   1.152  subsection\<open>Covering an open set by a countable chain of compact sets\<close>
   1.153    
   1.154 -proposition%important open_Union_compact_subsets:
   1.155 +proposition open_Union_compact_subsets:
   1.156    fixes S :: "'a::euclidean_space set"
   1.157    assumes "open S"
   1.158    obtains C where "\<And>n. compact(C n)" "\<And>n. C n \<subseteq> S"
   1.159                    "\<And>n. C n \<subseteq> interior(C(Suc n))"
   1.160                    "\<Union>(range C) = S"
   1.161                    "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. K \<subseteq> (C n)"
   1.162 -proof%unimportant (cases "S = {}")
   1.163 +proof (cases "S = {}")
   1.164    case True
   1.165    then show ?thesis
   1.166      by (rule_tac C = "\<lambda>n. {}" in that) auto