--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Jan 17 15:50:28 2019 +0000
@@ -13,7 +13,7 @@
"HOL-Library.FuncSet"
begin
-subsection%important \<open>Finite Cartesian products, with indexing and lambdas\<close>
+subsection%unimportant \<open>Finite Cartesian products, with indexing and lambdas\<close>
typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set"
morphisms vec_nth vec_lambda ..
@@ -104,10 +104,10 @@
by (auto elim!: countableE)
qed
-lemma infinite_UNIV_vec:
+lemma%important infinite_UNIV_vec:
assumes "infinite (UNIV :: 'a set)"
shows "infinite (UNIV :: ('a^'b) set)"
-proof (subst bij_betw_finite)
+proof%unimportant (subst bij_betw_finite)
show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
have "infinite (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" (is "infinite ?A")
@@ -125,9 +125,9 @@
finally show "infinite (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" .
qed
-lemma CARD_vec [simp]:
+lemma%important CARD_vec [simp]:
"CARD('a^'b) = CARD('a) ^ CARD('b)"
-proof (cases "finite (UNIV :: 'a set)")
+proof%unimportant (cases "finite (UNIV :: 'a set)")
case True
show ?thesis
proof (subst bij_betw_same_card)
@@ -143,7 +143,7 @@
qed
qed (simp_all add: infinite_UNIV_vec)
-lemma countable_vector:
+lemma%unimportant countable_vector:
fixes B:: "'n::finite \<Rightarrow> 'a set"
assumes "\<And>i. countable (B i)"
shows "countable {V. \<forall>i::'n::finite. V $ i \<in> B i}"
@@ -165,7 +165,7 @@
by (simp add: image_comp o_def vec_nth_inverse)
qed
-subsection%important \<open>Group operations and class instances\<close>
+subsection%unimportant \<open>Group operations and class instances\<close>
instantiation vec :: (zero, finite) zero
begin
@@ -230,7 +230,7 @@
by standard (simp_all add: vec_eq_iff)
-subsection%important\<open>Basic componentwise operations on vectors\<close>
+subsection%unimportant\<open>Basic componentwise operations on vectors\<close>
instantiation vec :: (times, finite) times
begin
@@ -295,12 +295,12 @@
text\<open>Also the scalar-vector multiplication.\<close>
-definition%important vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
+definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
where "c *s x = (\<chi> i. c * (x$i))"
text \<open>scalar product\<close>
-definition%important scalar_product :: "'a :: semiring_1 ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" where
+definition scalar_product :: "'a :: semiring_1 ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" where
"scalar_product v w = (\<Sum> i \<in> UNIV. v $ i * w $ i)"
@@ -311,7 +311,7 @@
definition%important "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
-lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)"
+lemma%important vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)"
unfolding scaleR_vec_def by simp
instance%unimportant
@@ -330,7 +330,7 @@
(\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
(\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"
-instance proof
+instance proof%unimportant
show "open (UNIV :: ('a ^ 'b) set)"
unfolding open_vec_def by auto
next
@@ -358,30 +358,30 @@
end
-lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}"
+lemma%unimportant open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}"
unfolding open_vec_def by auto
-lemma open_vimage_vec_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)"
+lemma%unimportant open_vimage_vec_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)"
unfolding open_vec_def
apply clarify
apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp)
done
-lemma closed_vimage_vec_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"
+lemma%unimportant closed_vimage_vec_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)"
unfolding closed_open vimage_Compl [symmetric]
by (rule open_vimage_vec_nth)
-lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
+lemma%unimportant closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
proof -
have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto
thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
by (simp add: closed_INT closed_vimage_vec_nth)
qed
-lemma tendsto_vec_nth [tendsto_intros]:
+lemma%important tendsto_vec_nth [tendsto_intros]:
assumes "((\<lambda>x. f x) \<longlongrightarrow> a) net"
shows "((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
-proof (rule topological_tendstoI)
+proof%unimportant (rule topological_tendstoI)
fix S assume "open S" "a $ i \<in> S"
then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"
by (simp_all add: open_vimage_vec_nth)
@@ -391,13 +391,13 @@
by simp
qed
-lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
+lemma%unimportant isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
unfolding isCont_def by (rule tendsto_vec_nth)
-lemma vec_tendstoI:
+lemma%important vec_tendstoI:
assumes "\<And>i. ((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
shows "((\<lambda>x. f x) \<longlongrightarrow> a) net"
-proof (rule topological_tendstoI)
+proof%unimportant (rule topological_tendstoI)
fix S assume "open S" and "a \<in> S"
then obtain A where A: "\<And>i. open (A i)" "\<And>i. a $ i \<in> A i"
and S: "\<And>y. \<forall>i. y $ i \<in> A i \<Longrightarrow> y \<in> S"
@@ -410,13 +410,13 @@
by (rule eventually_mono, simp add: S)
qed
-lemma tendsto_vec_lambda [tendsto_intros]:
+lemma%unimportant tendsto_vec_lambda [tendsto_intros]:
assumes "\<And>i. ((\<lambda>x. f x i) \<longlongrightarrow> a i) net"
shows "((\<lambda>x. \<chi> i. f x i) \<longlongrightarrow> (\<chi> i. a i)) net"
using assms by (simp add: vec_tendstoI)
-lemma open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)"
-proof (rule openI)
+lemma%important open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)"
+proof%unimportant (rule openI)
fix a assume "a \<in> (\<lambda>x. x $ i) ` S"
then obtain z where "a = z $ i" and "z \<in> S" ..
then obtain A where A: "\<forall>i. open (A i) \<and> z $ i \<in> A i"
@@ -470,10 +470,10 @@
instantiation%unimportant vec :: (metric_space, finite) metric_space
begin
-lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
+lemma%important dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
unfolding dist_vec_def by (rule member_le_L2_set) simp_all
-instance proof
+instance proof%unimportant
fix x y :: "'a ^ 'b"
show "dist x y = 0 \<longleftrightarrow> x = y"
unfolding dist_vec_def
@@ -532,15 +532,15 @@
end
-lemma Cauchy_vec_nth:
+lemma%important Cauchy_vec_nth:
"Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)"
unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_vec_nth_le])
-lemma vec_CauchyI:
+lemma%important vec_CauchyI:
fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n"
assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)"
shows "Cauchy (\<lambda>n. X n)"
-proof (rule metric_CauchyI)
+proof%unimportant (rule metric_CauchyI)
fix r :: real assume "0 < r"
hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp
define N where "N i = (LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s)" for i
@@ -591,7 +591,7 @@
definition%important "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
-instance proof
+instance proof%unimportant
fix a :: real and x y :: "'a ^ 'b"
show "norm x = 0 \<longleftrightarrow> x = 0"
unfolding norm_vec_def
@@ -613,32 +613,32 @@
end
-lemma norm_nth_le: "norm (x $ i) \<le> norm x"
+lemma%unimportant norm_nth_le: "norm (x $ i) \<le> norm x"
unfolding norm_vec_def
by (rule member_le_L2_set) simp_all
-lemma norm_le_componentwise_cart:
+lemma%important norm_le_componentwise_cart:
fixes x :: "'a::real_normed_vector^'n"
assumes "\<And>i. norm(x$i) \<le> norm(y$i)"
shows "norm x \<le> norm y"
- unfolding norm_vec_def
- by (rule L2_set_mono) (auto simp: assms)
+ unfolding%unimportant norm_vec_def
+ by%unimportant (rule L2_set_mono) (auto simp: assms)
-lemma component_le_norm_cart: "\<bar>x$i\<bar> \<le> norm x"
+lemma%unimportant component_le_norm_cart: "\<bar>x$i\<bar> \<le> norm x"
apply (simp add: norm_vec_def)
apply (rule member_le_L2_set, simp_all)
done
-lemma norm_bound_component_le_cart: "norm x \<le> e ==> \<bar>x$i\<bar> \<le> e"
+lemma%unimportant norm_bound_component_le_cart: "norm x \<le> e ==> \<bar>x$i\<bar> \<le> e"
by (metis component_le_norm_cart order_trans)
-lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
+lemma%unimportant norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
by (metis component_le_norm_cart le_less_trans)
-lemma norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
+lemma%unimportant norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
by (simp add: norm_vec_def L2_set_le_sum)
-lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
+lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
apply standard
apply (rule vector_add_component)
apply (rule vector_scaleR_component)
@@ -655,7 +655,7 @@
definition%important "inner x y = sum (\<lambda>i. inner (x$i) (y$i)) UNIV"
-instance proof
+instance proof%unimportant
fix r :: real and x y z :: "'a ^ 'b"
show "inner x y = inner y x"
unfolding inner_vec_def
@@ -686,13 +686,13 @@
definition%important "axis k x = (\<chi> i. if i = k then x else 0)"
-lemma axis_nth [simp]: "axis i x $ i = x"
+lemma%unimportant axis_nth [simp]: "axis i x $ i = x"
unfolding axis_def by simp
-lemma axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0"
+lemma%unimportant axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0"
unfolding axis_def vec_eq_iff by auto
-lemma inner_axis_axis:
+lemma%unimportant inner_axis_axis:
"inner (axis i x) (axis j y) = (if i = j then inner x y else 0)"
unfolding inner_vec_def
apply (cases "i = j")
@@ -702,10 +702,10 @@
apply (rule sum.neutral, simp add: axis_def)
done
-lemma inner_axis: "inner x (axis i y) = inner (x $ i) y"
+lemma%unimportant inner_axis: "inner x (axis i y) = inner (x $ i) y"
by (simp add: inner_vec_def axis_def sum.remove [where x=i])
-lemma inner_axis': "inner(axis i y) x = inner y (x $ i)"
+lemma%unimportant inner_axis': "inner(axis i y) x = inner y (x $ i)"
by (simp add: inner_axis inner_commute)
instantiation%unimportant vec :: (euclidean_space, finite) euclidean_space
@@ -713,7 +713,7 @@
definition%important "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})"
-instance proof
+instance proof%unimportant
show "(Basis :: ('a ^ 'b) set) \<noteq> {}"
unfolding Basis_vec_def by simp
next
@@ -732,8 +732,8 @@
by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
qed
-proposition DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
-proof -
+lemma%important DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
+proof%unimportant -
have "card (\<Union>i::'b. \<Union>u::'a\<in>Basis. {axis i u}) = (\<Sum>i::'b\<in>UNIV. card (\<Union>u::'a\<in>Basis. {axis i u}))"
by (rule card_UN_disjoint) (auto simp: axis_eq_axis)
also have "... = CARD('b) * DIM('a)"
@@ -744,30 +744,30 @@
end
-lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
+lemma%unimportant norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
by (simp add: inner_axis' norm_eq_1)
-lemma sum_norm_allsubsets_bound_cart:
+lemma%important sum_norm_allsubsets_bound_cart:
fixes f:: "'a \<Rightarrow> real ^'n"
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (sum f Q) \<le> e"
shows "sum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) * e"
- using sum_norm_allsubsets_bound[OF assms]
- by simp
+ using%unimportant sum_norm_allsubsets_bound[OF assms]
+ by%unimportant simp
-lemma cart_eq_inner_axis: "a $ i = inner a (axis i 1)"
+lemma%unimportant cart_eq_inner_axis: "a $ i = inner a (axis i 1)"
by (simp add: inner_axis)
-lemma axis_eq_0_iff [simp]:
+lemma%unimportant axis_eq_0_iff [simp]:
shows "axis m x = 0 \<longleftrightarrow> x = 0"
by (simp add: axis_def vec_eq_iff)
-lemma axis_in_Basis_iff [simp]: "axis i a \<in> Basis \<longleftrightarrow> a \<in> Basis"
+lemma%unimportant axis_in_Basis_iff [simp]: "axis i a \<in> Basis \<longleftrightarrow> a \<in> Basis"
by (auto simp: Basis_vec_def axis_eq_axis)
text\<open>Mapping each basis element to the corresponding finite index\<close>
definition axis_index :: "('a::comm_ring_1)^'n \<Rightarrow> 'n" where "axis_index v \<equiv> SOME i. v = axis i 1"
-lemma axis_inverse:
+lemma%unimportant axis_inverse:
fixes v :: "real^'n"
assumes "v \<in> Basis"
shows "\<exists>i. v = axis i 1"
@@ -778,20 +778,20 @@
by (force simp add: vec_eq_iff)
qed
-lemma axis_index:
+lemma%unimportant axis_index:
fixes v :: "real^'n"
assumes "v \<in> Basis"
shows "v = axis (axis_index v) 1"
by (metis (mono_tags) assms axis_inverse axis_index_def someI_ex)
-lemma axis_index_axis [simp]:
+lemma%unimportant axis_index_axis [simp]:
fixes UU :: "real^'n"
shows "(axis_index (axis u 1 :: real^'n)) = (u::'n)"
by (simp add: axis_eq_axis axis_index_def)
subsection%unimportant \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\<close>
-lemma sum_cong_aux:
+lemma%unimportant sum_cong_aux:
"(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> sum f A = sum g A"
by (auto intro: sum.cong)
@@ -823,22 +823,22 @@
end
\<close> "lift trivial vector statements to real arith statements"
-lemma vec_0[simp]: "vec 0 = 0" by vector
-lemma vec_1[simp]: "vec 1 = 1" by vector
+lemma%unimportant vec_0[simp]: "vec 0 = 0" by vector
+lemma%unimportant vec_1[simp]: "vec 1 = 1" by vector
-lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
+lemma%unimportant vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
-lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
+lemma%unimportant vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
-lemma vec_add: "vec(x + y) = vec x + vec y" by vector
-lemma vec_sub: "vec(x - y) = vec x - vec y" by vector
-lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
-lemma vec_neg: "vec(- x) = - vec x " by vector
+lemma%unimportant vec_add: "vec(x + y) = vec x + vec y" by vector
+lemma%unimportant vec_sub: "vec(x - y) = vec x - vec y" by vector
+lemma%unimportant vec_cmul: "vec(c * x) = c *s vec x " by vector
+lemma%unimportant vec_neg: "vec(- x) = - vec x " by vector
-lemma vec_scaleR: "vec(c * x) = c *\<^sub>R vec x"
+lemma%unimportant vec_scaleR: "vec(c * x) = c *\<^sub>R vec x"
by vector
-lemma vec_sum:
+lemma%unimportant vec_sum:
assumes "finite S"
shows "vec(sum f S) = sum (vec \<circ> f) S"
using assms
@@ -852,24 +852,24 @@
text\<open>Obvious "component-pushing".\<close>
-lemma vec_component [simp]: "vec x $ i = x"
+lemma%unimportant vec_component [simp]: "vec x $ i = x"
by vector
-lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
+lemma%unimportant vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
by vector
-lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)"
+lemma%unimportant vector_smult_component [simp]: "(c *s y)$i = c * (y$i)"
by vector
-lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
+lemma%unimportant cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
-lemmas vector_component =
+lemmas%unimportant vector_component =
vec_component vector_add_component vector_mult_component
vector_smult_component vector_minus_component vector_uminus_component
vector_scaleR_component cond_component
-subsection%important \<open>Some frequently useful arithmetic lemmas over vectors\<close>
+subsection%unimportant \<open>Some frequently useful arithmetic lemmas over vectors\<close>
instance vec :: (semigroup_mult, finite) semigroup_mult
by standard (vector mult.assoc)
@@ -1011,7 +1011,7 @@
definition%important map_matrix::"('a \<Rightarrow> 'b) \<Rightarrow> (('a, 'i::finite)vec, 'j::finite) vec \<Rightarrow> (('b, 'i)vec, 'j) vec" where
"map_matrix f x = (\<chi> i j. f (x $ i $ j))"
-lemma nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)"
+lemma%unimportant nth_map_matrix[simp]: "map_matrix f x $ i $ j = f (x $ i $ j)"
by (simp add: map_matrix_def)
definition%important matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
@@ -1034,17 +1034,17 @@
definition%unimportant "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
definition%unimportant "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"
-lemma times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0"
+lemma%unimportant times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0"
by (simp add: matrix_matrix_mult_def zero_vec_def)
-lemma times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0"
+lemma%unimportant times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0"
by (simp add: matrix_matrix_mult_def zero_vec_def)
-lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
-lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
+lemma%unimportant mat_0[simp]: "mat 0 = 0" by (vector mat_def)
+lemma%unimportant matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)
-lemma matrix_mul_lid [simp]:
+lemma%unimportant matrix_mul_lid [simp]:
fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
shows "mat 1 ** A = A"
apply (simp add: matrix_matrix_mult_def mat_def)
@@ -1053,7 +1053,7 @@
mult_1_left mult_zero_left if_True UNIV_I)
done
-lemma matrix_mul_rid [simp]:
+lemma%unimportant matrix_mul_rid [simp]:
fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
shows "A ** mat 1 = A"
apply (simp add: matrix_matrix_mult_def mat_def)
@@ -1062,39 +1062,47 @@
mult_1_right mult_zero_right if_True UNIV_I cong: if_cong)
done
-proposition matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
+lemma%unimportant matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C"
apply (vector matrix_matrix_mult_def sum_distrib_left sum_distrib_right mult.assoc)
apply (subst sum.swap)
apply simp
done
-proposition matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
+lemma%unimportant matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
apply (vector matrix_matrix_mult_def matrix_vector_mult_def
sum_distrib_left sum_distrib_right mult.assoc)
apply (subst sum.swap)
apply simp
done
-lemma scalar_matrix_assoc:
+lemma%unimportant scalar_matrix_assoc:
fixes A :: "('a::real_algebra_1)^'m^'n"
shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B"
by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff scaleR_sum_right)
-lemma matrix_scalar_ac:
+lemma%unimportant matrix_scalar_ac:
fixes A :: "('a::real_algebra_1)^'m^'n"
shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B"
by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)
-lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
+lemma%unimportant matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
apply (vector matrix_vector_mult_def mat_def)
apply (simp add: if_distrib if_distribR sum.delta' cong del: if_weak_cong)
done
-lemma matrix_transpose_mul:
+lemma%unimportant matrix_transpose_mul:
"transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult.commute)
-lemma matrix_eq:
+lemma%unimportant matrix_mult_transpose_dot_column:
+ shows "transpose A ** A = (\<chi> i j. inner (column i A) (column j A))"
+ by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
+
+lemma%unimportant matrix_mult_transpose_dot_row:
+ shows "A ** transpose A = (\<chi> i j. inner (row i A) (row j A))"
+ by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
+
+lemma%unimportant matrix_eq:
fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
shows "A = B \<longleftrightarrow> (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
apply auto
@@ -1107,49 +1115,49 @@
sum.delta[OF finite] cong del: if_weak_cong)
done
-lemma matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x"
+lemma%unimportant matrix_vector_mul_component: "(A *v x)$k = inner (A$k) x"
by (simp add: matrix_vector_mult_def inner_vec_def)
-lemma dot_lmul_matrix: "inner ((x::real ^_) v* A) y = inner x (A *v y)"
+lemma%unimportant dot_lmul_matrix: "inner ((x::real ^_) v* A) y = inner x (A *v y)"
apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps)
apply (subst sum.swap)
apply simp
done
-lemma transpose_mat [simp]: "transpose (mat n) = mat n"
+lemma%unimportant transpose_mat [simp]: "transpose (mat n) = mat n"
by (vector transpose_def mat_def)
-lemma transpose_transpose [simp]: "transpose(transpose A) = A"
+lemma%unimportant transpose_transpose [simp]: "transpose(transpose A) = A"
by (vector transpose_def)
-lemma row_transpose [simp]: "row i (transpose A) = column i A"
+lemma%unimportant row_transpose [simp]: "row i (transpose A) = column i A"
by (simp add: row_def column_def transpose_def vec_eq_iff)
-lemma column_transpose [simp]: "column i (transpose A) = row i A"
+lemma%unimportant column_transpose [simp]: "column i (transpose A) = row i A"
by (simp add: row_def column_def transpose_def vec_eq_iff)
-lemma rows_transpose [simp]: "rows(transpose A) = columns A"
+lemma%unimportant rows_transpose [simp]: "rows(transpose A) = columns A"
by (auto simp add: rows_def columns_def intro: set_eqI)
-lemma columns_transpose [simp]: "columns(transpose A) = rows A"
+lemma%unimportant columns_transpose [simp]: "columns(transpose A) = rows A"
by (metis transpose_transpose rows_transpose)
-lemma transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A"
+lemma%unimportant transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A"
unfolding transpose_def
by (simp add: vec_eq_iff)
-lemma transpose_iff [iff]: "transpose A = transpose B \<longleftrightarrow> A = B"
+lemma%unimportant transpose_iff [iff]: "transpose A = transpose B \<longleftrightarrow> A = B"
by (metis transpose_transpose)
-lemma matrix_mult_sum:
+lemma%unimportant matrix_mult_sum:
"(A::'a::comm_semiring_1^'n^'m) *v x = sum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult.commute)
-lemma vector_componentwise:
+lemma%unimportant vector_componentwise:
"(x::'a::ring_1^'n) = (\<chi> j. \<Sum>i\<in>UNIV. (x$i) * (axis i 1 :: 'a^'n) $ j)"
by (simp add: axis_def if_distrib sum.If_cases vec_eq_iff)
-lemma basis_expansion: "sum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)"
+lemma%unimportant basis_expansion: "sum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)"
by (auto simp add: axis_def vec_eq_iff if_distrib sum.If_cases cong del: if_weak_cong)
@@ -1158,51 +1166,51 @@
definition%important matrix :: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
where "matrix f = (\<chi> i j. (f(axis j 1))$i)"
-lemma matrix_id_mat_1: "matrix id = mat 1"
+lemma%unimportant matrix_id_mat_1: "matrix id = mat 1"
by (simp add: mat_def matrix_def axis_def)
-lemma matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r"
+lemma%unimportant matrix_scaleR: "(matrix ((*\<^sub>R) r)) = mat r"
by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
-lemma matrix_vector_mul_linear[intro, simp]: "linear (\<lambda>x. A *v (x::'a::real_algebra_1 ^ _))"
+lemma%unimportant matrix_vector_mul_linear[intro, simp]: "linear (\<lambda>x. A *v (x::'a::real_algebra_1 ^ _))"
by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum_distrib_left
sum.distrib scaleR_right.sum)
-lemma vector_matrix_left_distrib [algebra_simps]:
+lemma%unimportant vector_matrix_left_distrib [algebra_simps]:
shows "(x + y) v* A = x v* A + y v* A"
unfolding vector_matrix_mult_def
by (simp add: algebra_simps sum.distrib vec_eq_iff)
-lemma matrix_vector_right_distrib [algebra_simps]:
+lemma%unimportant matrix_vector_right_distrib [algebra_simps]:
"A *v (x + y) = A *v x + A *v y"
by (vector matrix_vector_mult_def sum.distrib distrib_left)
-lemma matrix_vector_mult_diff_distrib [algebra_simps]:
+lemma%unimportant matrix_vector_mult_diff_distrib [algebra_simps]:
fixes A :: "'a::ring_1^'n^'m"
shows "A *v (x - y) = A *v x - A *v y"
by (vector matrix_vector_mult_def sum_subtractf right_diff_distrib)
-lemma matrix_vector_mult_scaleR[algebra_simps]:
+lemma%unimportant matrix_vector_mult_scaleR[algebra_simps]:
fixes A :: "real^'n^'m"
shows "A *v (c *\<^sub>R x) = c *\<^sub>R (A *v x)"
using linear_iff matrix_vector_mul_linear by blast
-lemma matrix_vector_mult_0_right [simp]: "A *v 0 = 0"
+lemma%unimportant matrix_vector_mult_0_right [simp]: "A *v 0 = 0"
by (simp add: matrix_vector_mult_def vec_eq_iff)
-lemma matrix_vector_mult_0 [simp]: "0 *v w = 0"
+lemma%unimportant matrix_vector_mult_0 [simp]: "0 *v w = 0"
by (simp add: matrix_vector_mult_def vec_eq_iff)
-lemma matrix_vector_mult_add_rdistrib [algebra_simps]:
+lemma%unimportant matrix_vector_mult_add_rdistrib [algebra_simps]:
"(A + B) *v x = (A *v x) + (B *v x)"
by (vector matrix_vector_mult_def sum.distrib distrib_right)
-lemma matrix_vector_mult_diff_rdistrib [algebra_simps]:
+lemma%unimportant matrix_vector_mult_diff_rdistrib [algebra_simps]:
fixes A :: "'a :: ring_1^'n^'m"
shows "(A - B) *v x = (A *v x) - (B *v x)"
by (vector matrix_vector_mult_def sum_subtractf left_diff_distrib)
-lemma matrix_vector_column:
+lemma%unimportant matrix_vector_column:
"(A::'a::comm_semiring_1^'n^_) *v x = sum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult.commute)
@@ -1215,17 +1223,17 @@
"matrix_inv(A:: 'a::semiring_1^'n^'m) =
(SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
-lemma inj_matrix_vector_mult:
+lemma%unimportant inj_matrix_vector_mult:
fixes A::"'a::field^'n^'m"
assumes "invertible A"
shows "inj ((*v) A)"
by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)
-lemma scalar_invertible:
+lemma%important scalar_invertible:
fixes A :: "('a::real_algebra_1)^'m^'n"
assumes "k \<noteq> 0" and "invertible A"
shows "invertible (k *\<^sub>R A)"
-proof -
+proof%unimportant -
obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
using assms unfolding invertible_def by auto
with \<open>k \<noteq> 0\<close>
@@ -1235,50 +1243,50 @@
unfolding invertible_def by auto
qed
-lemma scalar_invertible_iff:
+lemma%unimportant scalar_invertible_iff:
fixes A :: "('a::real_algebra_1)^'m^'n"
assumes "k \<noteq> 0" and "invertible A"
shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
by (simp add: assms scalar_invertible)
-lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
+lemma%unimportant vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
by simp
-lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
+lemma%unimportant transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
by simp
-lemma vector_scalar_commute:
+lemma%unimportant vector_scalar_commute:
fixes A :: "'a::{field}^'m^'n"
shows "A *v (c *s x) = c *s (A *v x)"
by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left)
-lemma scalar_vector_matrix_assoc:
+lemma%unimportant scalar_vector_matrix_assoc:
fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
shows "(k *s x) v* A = k *s (x v* A)"
by (metis transpose_matrix_vector vector_scalar_commute)
-lemma vector_matrix_mult_0 [simp]: "0 v* A = 0"
+lemma%unimportant vector_matrix_mult_0 [simp]: "0 v* A = 0"
unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
-lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
+lemma%unimportant vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
-lemma vector_matrix_mul_rid [simp]:
+lemma%unimportant vector_matrix_mul_rid [simp]:
fixes v :: "('a::semiring_1)^'n"
shows "v v* mat 1 = v"
by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
-lemma scaleR_vector_matrix_assoc:
+lemma%unimportant scaleR_vector_matrix_assoc:
fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
-lemma vector_scaleR_matrix_ac:
+lemma%important vector_scaleR_matrix_ac:
fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
-proof -
+proof%unimportant -
have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
unfolding vector_matrix_mult_def
by (simp add: algebra_simps)
--- a/src/HOL/Analysis/Further_Topology.thy Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy Thu Jan 17 15:50:28 2019 +0000
@@ -1,4 +1,4 @@
-section%important \<open>Extending Continous Maps, Invariance of Domain, etc\<close>
+section%important \<open>Extending Continous Maps, Invariance of Domain, etc\<close> (*FIX rename? *)
text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
@@ -8,13 +8,13 @@
subsection%important\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>
-lemma%important spheremap_lemma1:
+lemma spheremap_lemma1:
fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
assumes "subspace S" "subspace T" and dimST: "dim S < dim T"
and "S \<subseteq> T"
and diff_f: "f differentiable_on sphere 0 1 \<inter> S"
shows "f ` (sphere 0 1 \<inter> S) \<noteq> sphere 0 1 \<inter> T"
-proof%unimportant
+proof
assume fim: "f ` (sphere 0 1 \<inter> S) = sphere 0 1 \<inter> T"
have inS: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x /\<^sub>R norm x) \<in> S"
using subspace_mul \<open>subspace S\<close> by blast
@@ -158,14 +158,14 @@
qed
-lemma%important spheremap_lemma2:
+lemma spheremap_lemma2:
fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
assumes ST: "subspace S" "subspace T" "dim S < dim T"
and "S \<subseteq> T"
and contf: "continuous_on (sphere 0 1 \<inter> S) f"
and fim: "f ` (sphere 0 1 \<inter> S) \<subseteq> sphere 0 1 \<inter> T"
shows "\<exists>c. homotopic_with (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)"
-proof%unimportant -
+proof -
have [simp]: "\<And>x. \<lbrakk>norm x = 1; x \<in> S\<rbrakk> \<Longrightarrow> norm (f x) = 1"
using fim by (simp add: image_subset_iff)
have "compact (sphere 0 1 \<inter> S)"
@@ -252,11 +252,11 @@
qed
-lemma%important spheremap_lemma3:
+lemma spheremap_lemma3:
assumes "bounded S" "convex S" "subspace U" and affSU: "aff_dim S \<le> dim U"
obtains T where "subspace T" "T \<subseteq> U" "S \<noteq> {} \<Longrightarrow> aff_dim T = aff_dim S"
"(rel_frontier S) homeomorphic (sphere 0 1 \<inter> T)"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True
with \<open>subspace U\<close> subspace_0 show ?thesis
by (rule_tac T = "{0}" in that) auto
@@ -300,14 +300,14 @@
qed
-proposition%important inessential_spheremap_lowdim_gen:
+proposition inessential_spheremap_lowdim_gen:
fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space"
assumes "convex S" "bounded S" "convex T" "bounded T"
and affST: "aff_dim S < aff_dim T"
and contf: "continuous_on (rel_frontier S) f"
and fim: "f ` (rel_frontier S) \<subseteq> rel_frontier T"
obtains c where "homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True
then show ?thesis
by (simp add: that)
@@ -350,7 +350,7 @@
qed
qed
-lemma%unimportant inessential_spheremap_lowdim:
+lemma inessential_spheremap_lowdim:
fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space"
assumes
"DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \<subseteq> (sphere b s)"
@@ -379,7 +379,7 @@
subsection%important\<open> Some technical lemmas about extending maps from cell complexes\<close>
-lemma%unimportant extending_maps_Union_aux:
+lemma extending_maps_Union_aux:
assumes fin: "finite \<F>"
and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
and "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>; S \<noteq> T\<rbrakk> \<Longrightarrow> S \<inter> T \<subseteq> K"
@@ -410,7 +410,7 @@
done
qed
-lemma%unimportant extending_maps_Union:
+lemma extending_maps_Union:
assumes fin: "finite \<F>"
and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S"
@@ -422,14 +422,14 @@
by (metis K psubsetI)
-lemma%important extend_map_lemma:
+lemma extend_map_lemma:
assumes "finite \<F>" "\<G> \<subseteq> \<F>" "convex T" "bounded T"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F> - \<G> \<Longrightarrow> aff_dim X < aff_dim T"
and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T"
and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
obtains g where "continuous_on (\<Union>\<F>) g" "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
-proof%unimportant (cases "\<F> - \<G> = {}")
+proof (cases "\<F> - \<G> = {}")
case True
then have "\<Union>\<F> \<subseteq> \<Union>\<G>"
by (simp add: Union_mono)
@@ -608,7 +608,7 @@
using extendf [of i] unfolding eq by (metis that)
qed
-lemma%unimportant extend_map_lemma_cofinite0:
+lemma extend_map_lemma_cofinite0:
assumes "finite \<F>"
and "pairwise (\<lambda>S T. S \<inter> T \<subseteq> K) \<F>"
and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S - {a}) g \<and> g ` (S - {a}) \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)"
@@ -665,7 +665,7 @@
qed
-lemma%unimportant extend_map_lemma_cofinite1:
+lemma extend_map_lemma_cofinite1:
assumes "finite \<F>"
and \<F>: "\<And>X. X \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (X - {a}) g \<and> g ` (X - {a}) \<subseteq> T \<and> (\<forall>x \<in> X \<inter> K. g x = h x)"
and clo: "\<And>X. X \<in> \<F> \<Longrightarrow> closed X"
@@ -695,7 +695,7 @@
qed
-lemma%important extend_map_lemma_cofinite:
+lemma extend_map_lemma_cofinite:
assumes "finite \<F>" "\<G> \<subseteq> \<F>" and T: "convex T" "bounded T"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T"
@@ -704,7 +704,7 @@
obtains C g where
"finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F> - C) g"
"g ` (\<Union> \<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x"
-proof%unimportant -
+proof -
define \<H> where "\<H> \<equiv> \<G> \<union> {D. \<exists>C \<in> \<F> - \<G>. D face_of C \<and> aff_dim D < aff_dim T}"
have "finite \<G>"
using assms finite_subset by blast
@@ -869,7 +869,7 @@
qed
text\<open>The next two proofs are similar\<close>
-theorem%important extend_map_cell_complex_to_sphere:
+theorem extend_map_cell_complex_to_sphere:
assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X < aff_dim T"
@@ -877,7 +877,7 @@
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
obtains g where "continuous_on (\<Union>\<F>) g"
"g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant -
+proof -
obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g ` V \<subseteq> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
have "compact S"
@@ -924,7 +924,7 @@
qed
-theorem%important extend_map_cell_complex_to_sphere_cofinite:
+theorem extend_map_cell_complex_to_sphere_cofinite:
assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T"
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> aff_dim T"
@@ -932,7 +932,7 @@
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T"
obtains C g where "finite C" "disjnt C S" "continuous_on (\<Union>\<F> - C) g"
"g ` (\<Union>\<F> - C) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant -
+proof -
obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g ` V \<subseteq> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast
have "compact S"
@@ -993,10 +993,10 @@
subsection%important\<open> Special cases and corollaries involving spheres\<close>
-lemma%unimportant disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
+lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
by (auto simp: disjnt_def)
-proposition%important extend_map_affine_to_sphere_cofinite_simple:
+proposition extend_map_affine_to_sphere_cofinite_simple:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "compact S" "convex U" "bounded U"
and aff: "aff_dim T \<le> aff_dim U"
@@ -1005,7 +1005,7 @@
obtains K g where "finite K" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
"g ` (T - K) \<subseteq> rel_frontier U"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant -
+proof -
have "\<exists>K g. finite K \<and> disjnt K S \<and> continuous_on (T - K) g \<and>
g ` (T - K) \<subseteq> rel_frontier U \<and> (\<forall>x \<in> S. g x = f x)"
if "affine T" "S \<subseteq> T" and aff: "aff_dim T \<le> aff_dim U" for T
@@ -1144,14 +1144,14 @@
(*Up to extend_map_affine_to_sphere_cofinite_gen*)
-lemma%important extend_map_affine_to_sphere1:
+lemma extend_map_affine_to_sphere1:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::topological_space"
assumes "finite K" "affine U" and contf: "continuous_on (U - K) f"
and fim: "f ` (U - K) \<subseteq> T"
and comps: "\<And>C. \<lbrakk>C \<in> components(U - S); C \<inter> K \<noteq> {}\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
and clo: "closedin (subtopology euclidean U) S" and K: "disjnt K S" "K \<subseteq> U"
obtains g where "continuous_on (U - L) g" "g ` (U - L) \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant (cases "K = {}")
+proof (cases "K = {}")
case True
then show ?thesis
by (metis Diff_empty Diff_subset contf fim continuous_on_subset image_subsetI rev_image_eqI subset_iff that)
@@ -1436,7 +1436,7 @@
qed
-lemma%important extend_map_affine_to_sphere2:
+lemma extend_map_affine_to_sphere2:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "compact S" "convex U" "bounded U" "affine T" "S \<subseteq> T"
and affTU: "aff_dim T \<le> aff_dim U"
@@ -1446,7 +1446,7 @@
obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S"
"continuous_on (T - K) g" "g ` (T - K) \<subseteq> rel_frontier U"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant -
+proof -
obtain K g where K: "finite K" "K \<subseteq> T" "disjnt K S"
and contg: "continuous_on (T - K) g"
and gim: "g ` (T - K) \<subseteq> rel_frontier U"
@@ -1490,7 +1490,7 @@
qed
-proposition%important extend_map_affine_to_sphere_cofinite_gen:
+proposition extend_map_affine_to_sphere_cofinite_gen:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes SUT: "compact S" "convex U" "bounded U" "affine T" "S \<subseteq> T"
and aff: "aff_dim T \<le> aff_dim U"
@@ -1500,7 +1500,7 @@
obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
"g ` (T - K) \<subseteq> rel_frontier U"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True
show ?thesis
proof (cases "rel_frontier U = {}")
@@ -1645,7 +1645,7 @@
qed
-corollary%important extend_map_affine_to_sphere_cofinite:
+corollary extend_map_affine_to_sphere_cofinite:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes SUT: "compact S" "affine T" "S \<subseteq> T"
and aff: "aff_dim T \<le> DIM('b)" and "0 \<le> r"
@@ -1654,7 +1654,7 @@
and dis: "\<And>C. \<lbrakk>C \<in> components(T - S); bounded C\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}"
obtains K g where "finite K" "K \<subseteq> L" "K \<subseteq> T" "disjnt K S" "continuous_on (T - K) g"
"g ` (T - K) \<subseteq> sphere a r" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof%unimportant (cases "r = 0")
+proof (cases "r = 0")
case True
with fim show ?thesis
by (rule_tac K="{}" and g = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
@@ -1670,7 +1670,7 @@
done
qed
-corollary%important extend_map_UNIV_to_sphere_cofinite:
+corollary extend_map_UNIV_to_sphere_cofinite:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes aff: "DIM('a) \<le> DIM('b)" and "0 \<le> r"
and SUT: "compact S"
@@ -1684,7 +1684,7 @@
apply (auto simp: assms that Compl_eq_Diff_UNIV [symmetric])
done
-corollary%important extend_map_UNIV_to_sphere_no_bounded_component:
+corollary extend_map_UNIV_to_sphere_no_bounded_component:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes aff: "DIM('a) \<le> DIM('b)" and "0 \<le> r"
and SUT: "compact S"
@@ -1696,14 +1696,14 @@
apply (auto simp: that dest: dis)
done
-theorem%important Borsuk_separation_theorem_gen:
+theorem Borsuk_separation_theorem_gen:
fixes S :: "'a::euclidean_space set"
assumes "compact S"
shows "(\<forall>c \<in> components(- S). \<not>bounded c) \<longleftrightarrow>
(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
\<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
(is "?lhs = ?rhs")
-proof%unimportant
+proof
assume L [rule_format]: ?lhs
show ?rhs
proof clarify
@@ -1734,14 +1734,14 @@
qed
-corollary%important Borsuk_separation_theorem:
+corollary Borsuk_separation_theorem:
fixes S :: "'a::euclidean_space set"
assumes "compact S" and 2: "2 \<le> DIM('a)"
shows "connected(- S) \<longleftrightarrow>
(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
\<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
(is "?lhs = ?rhs")
-proof%unimportant
+proof
assume L: ?lhs
show ?rhs
proof (cases "S = {}")
@@ -1764,7 +1764,7 @@
qed
-lemma%unimportant homotopy_eqv_separation:
+lemma homotopy_eqv_separation:
fixes S :: "'a::euclidean_space set" and T :: "'a set"
assumes "S homotopy_eqv T" and "compact S" and "compact T"
shows "connected(- S) \<longleftrightarrow> connected(- T)"
@@ -1783,11 +1783,11 @@
qed
qed
-lemma%important Jordan_Brouwer_separation:
+proposition Jordan_Brouwer_separation:
fixes S :: "'a::euclidean_space set" and a::'a
assumes hom: "S homeomorphic sphere a r" and "0 < r"
shows "\<not> connected(- S)"
-proof%unimportant -
+proof -
have "- sphere a r \<inter> ball a r \<noteq> {}"
using \<open>0 < r\<close> by (simp add: Int_absorb1 subset_eq)
moreover
@@ -1817,11 +1817,11 @@
qed
-lemma%important Jordan_Brouwer_frontier:
+proposition Jordan_Brouwer_frontier:
fixes S :: "'a::euclidean_space set" and a::'a
assumes S: "S homeomorphic sphere a r" and T: "T \<in> components(- S)" and 2: "2 \<le> DIM('a)"
shows "frontier T = S"
-proof%unimportant (cases r rule: linorder_cases)
+proof (cases r rule: linorder_cases)
assume "r < 0"
with S T show ?thesis by auto
next
@@ -1866,11 +1866,11 @@
qed (rule T)
qed
-lemma%important Jordan_Brouwer_nonseparation:
+proposition Jordan_Brouwer_nonseparation:
fixes S :: "'a::euclidean_space set" and a::'a
assumes S: "S homeomorphic sphere a r" and "T \<subset> S" and 2: "2 \<le> DIM('a)"
shows "connected(- T)"
-proof%unimportant -
+proof -
have *: "connected(C \<union> (S - T))" if "C \<in> components(- S)" for C
proof (rule connected_intermediate_closure)
show "connected C"
@@ -1894,7 +1894,7 @@
subsection%important\<open> Invariance of domain and corollaries\<close>
-lemma%unimportant invariance_of_domain_ball:
+lemma invariance_of_domain_ball:
fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
assumes contf: "continuous_on (cball a r) f" and "0 < r"
and inj: "inj_on f (cball a r)"
@@ -1983,12 +1983,12 @@
text\<open>Proved by L. E. J. Brouwer (1912)\<close>
-theorem%important invariance_of_domain:
+theorem invariance_of_domain:
fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
assumes "continuous_on S f" "open S" "inj_on f S"
shows "open(f ` S)"
unfolding open_subopen [of "f`S"]
-proof%unimportant clarify
+proof clarify
fix a
assume "a \<in> S"
obtain \<delta> where "\<delta> > 0" and \<delta>: "cball a \<delta> \<subseteq> S"
@@ -2004,7 +2004,7 @@
qed
qed
-lemma%unimportant inv_of_domain_ss0:
+lemma inv_of_domain_ss0:
fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
and "subspace S" and dimS: "dim S = DIM('b::euclidean_space)"
@@ -2049,7 +2049,7 @@
by (metis (no_types, hide_lams) homeomorphism_imp_open_map homhk image_comp open_openin subtopology_UNIV)
qed
-lemma%unimportant inv_of_domain_ss1:
+lemma inv_of_domain_ss1:
fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
assumes contf: "continuous_on U f" and injf: "inj_on f U" and fim: "f ` U \<subseteq> S"
and "subspace S"
@@ -2090,14 +2090,14 @@
qed
-corollary%important invariance_of_domain_subspaces:
+corollary invariance_of_domain_subspaces:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes ope: "openin (subtopology euclidean U) S"
and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
and injf: "inj_on f S"
shows "openin (subtopology euclidean V) (f ` S)"
-proof%unimportant -
+proof -
obtain V' where "subspace V'" "V' \<subseteq> U" "dim V' = dim V"
using choose_subspace_of_subspace [OF VU]
by (metis span_eq_iff \<open>subspace U\<close>)
@@ -2134,14 +2134,14 @@
qed
qed
-corollary%important invariance_of_dimension_subspaces:
+corollary invariance_of_dimension_subspaces:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes ope: "openin (subtopology euclidean U) S"
and "subspace U" "subspace V"
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
and injf: "inj_on f S" and "S \<noteq> {}"
shows "dim U \<le> dim V"
-proof%unimportant -
+proof -
have "False" if "dim V < dim U"
proof -
obtain T where "subspace T" "T \<subseteq> U" "dim T = dim V"
@@ -2174,14 +2174,14 @@
using not_less by blast
qed
-corollary%important invariance_of_domain_affine_sets:
+corollary invariance_of_domain_affine_sets:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes ope: "openin (subtopology euclidean U) S"
and aff: "affine U" "affine V" "aff_dim V \<le> aff_dim U"
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
and injf: "inj_on f S"
shows "openin (subtopology euclidean V) (f ` S)"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True
then show ?thesis by auto
next
@@ -2209,14 +2209,14 @@
by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois)
qed
-corollary%important invariance_of_dimension_affine_sets:
+corollary invariance_of_dimension_affine_sets:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes ope: "openin (subtopology euclidean U) S"
and aff: "affine U" "affine V"
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
and injf: "inj_on f S" and "S \<noteq> {}"
shows "aff_dim U \<le> aff_dim V"
-proof%unimportant -
+proof -
obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
using \<open>S \<noteq> {}\<close> fim ope openin_contains_cball by fastforce
have "dim ((+) (- a) ` U) \<le> dim ((+) (- b) ` V)"
@@ -2238,7 +2238,7 @@
by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
qed
-corollary%important invariance_of_dimension:
+corollary invariance_of_dimension:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes contf: "continuous_on S f" and "open S"
and injf: "inj_on f S" and "S \<noteq> {}"
@@ -2247,7 +2247,7 @@
by auto
-corollary%important continuous_injective_image_subspace_dim_le:
+corollary continuous_injective_image_subspace_dim_le:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "subspace S" "subspace T"
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
@@ -2256,7 +2256,7 @@
apply (rule invariance_of_dimension_subspaces [of S S _ f])
using%unimportant assms by (auto simp: subspace_affine)
-lemma%unimportant invariance_of_dimension_convex_domain:
+lemma invariance_of_dimension_convex_domain:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "convex S"
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> affine hull T"
@@ -2285,7 +2285,7 @@
qed
-lemma%unimportant homeomorphic_convex_sets_le:
+lemma homeomorphic_convex_sets_le:
assumes "convex S" "S homeomorphic T"
shows "aff_dim S \<le> aff_dim T"
proof -
@@ -2302,23 +2302,23 @@
qed
qed
-lemma%unimportant homeomorphic_convex_sets:
+lemma homeomorphic_convex_sets:
assumes "convex S" "convex T" "S homeomorphic T"
shows "aff_dim S = aff_dim T"
by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym)
-lemma%unimportant homeomorphic_convex_compact_sets_eq:
+lemma homeomorphic_convex_compact_sets_eq:
assumes "convex S" "compact S" "convex T" "compact T"
shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets)
-lemma%unimportant invariance_of_domain_gen:
+lemma invariance_of_domain_gen:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
shows "open(f ` S)"
using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto
-lemma%unimportant injective_into_1d_imp_open_map_UNIV:
+lemma injective_into_1d_imp_open_map_UNIV:
fixes f :: "'a::euclidean_space \<Rightarrow> real"
assumes "open T" "continuous_on S f" "inj_on f S" "T \<subseteq> S"
shows "open (f ` T)"
@@ -2326,7 +2326,7 @@
using assms apply (auto simp: elim: continuous_on_subset subset_inj_on)
done
-lemma%unimportant continuous_on_inverse_open:
+lemma continuous_on_inverse_open:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" and gf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
shows "continuous_on (f ` S) g"
@@ -2345,7 +2345,7 @@
by (metis \<open>open T\<close> continuous_on_subset inj_onI inj_on_subset invariance_of_domain_gen openin_open openin_open_eq)
qed
-lemma%unimportant invariance_of_domain_homeomorphism:
+lemma invariance_of_domain_homeomorphism:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
obtains g where "homeomorphism S (f ` S) f g"
@@ -2354,14 +2354,14 @@
by (simp add: assms continuous_on_inverse_open homeomorphism_def)
qed
-corollary%important invariance_of_domain_homeomorphic:
+corollary invariance_of_domain_homeomorphic:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
shows "S homeomorphic (f ` S)"
using%unimportant invariance_of_domain_homeomorphism [OF assms]
by%unimportant (meson homeomorphic_def)
-lemma%unimportant continuous_image_subset_interior:
+lemma continuous_image_subset_interior:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
shows "f ` (interior S) \<subseteq> interior(f ` S)"
@@ -2372,13 +2372,13 @@
apply (auto simp: subset_inj_on interior_subset continuous_on_subset)
done
-lemma%important homeomorphic_interiors_same_dimension:
+lemma homeomorphic_interiors_same_dimension:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)"
shows "(interior S) homeomorphic (interior T)"
using assms [unfolded homeomorphic_minimal]
unfolding homeomorphic_def
-proof%unimportant (clarify elim!: ex_forward)
+proof (clarify elim!: ex_forward)
fix f g
assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
and contf: "continuous_on S f" and contg: "continuous_on T g"
@@ -2422,7 +2422,7 @@
qed
qed
-lemma%unimportant homeomorphic_open_imp_same_dimension:
+lemma homeomorphic_open_imp_same_dimension:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "S homeomorphic T" "open S" "S \<noteq> {}" "open T" "T \<noteq> {}"
shows "DIM('a) = DIM('b)"
@@ -2431,7 +2431,7 @@
apply (rule order_antisym; metis inj_onI invariance_of_dimension)
done
-lemma%unimportant homeomorphic_interiors:
+proposition homeomorphic_interiors:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "S homeomorphic T" "interior S = {} \<longleftrightarrow> interior T = {}"
shows "(interior S) homeomorphic (interior T)"
@@ -2449,7 +2449,7 @@
by (rule homeomorphic_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
qed
-lemma%unimportant homeomorphic_frontiers_same_dimension:
+lemma homeomorphic_frontiers_same_dimension:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)"
shows "(frontier S) homeomorphic (frontier T)"
@@ -2505,7 +2505,7 @@
qed
qed
-lemma%unimportant homeomorphic_frontiers:
+lemma homeomorphic_frontiers:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "S homeomorphic T" "closed S" "closed T"
"interior S = {} \<longleftrightarrow> interior T = {}"
@@ -2522,7 +2522,7 @@
using False assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast
qed
-lemma%unimportant continuous_image_subset_rel_interior:
+lemma continuous_image_subset_rel_interior:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
and TS: "aff_dim T \<le> aff_dim S"
@@ -2545,7 +2545,7 @@
qed auto
qed
-lemma%unimportant homeomorphic_rel_interiors_same_dimension:
+lemma homeomorphic_rel_interiors_same_dimension:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
shows "(rel_interior S) homeomorphic (rel_interior T)"
@@ -2597,11 +2597,11 @@
qed
qed
-lemma%important homeomorphic_rel_interiors:
+lemma homeomorphic_rel_interiors:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
shows "(rel_interior S) homeomorphic (rel_interior T)"
-proof%unimportant (cases "rel_interior T = {}")
+proof (cases "rel_interior T = {}")
case True
with assms show ?thesis by auto
next
@@ -2630,7 +2630,7 @@
qed
-lemma%unimportant homeomorphic_rel_boundaries_same_dimension:
+lemma homeomorphic_rel_boundaries_same_dimension:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
@@ -2664,7 +2664,7 @@
qed
qed
-lemma%unimportant homeomorphic_rel_boundaries:
+lemma homeomorphic_rel_boundaries:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
@@ -2696,11 +2696,11 @@
by (rule homeomorphic_rel_boundaries_same_dimension [OF \<open>S homeomorphic T\<close>])
qed
-proposition%important uniformly_continuous_homeomorphism_UNIV_trivial:
+proposition uniformly_continuous_homeomorphism_UNIV_trivial:
fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g"
shows "S = UNIV"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True
then show ?thesis
by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI)
@@ -2744,7 +2744,7 @@
subsection%important\<open>Dimension-based conditions for various homeomorphisms\<close>
-lemma%unimportant homeomorphic_subspaces_eq:
+lemma homeomorphic_subspaces_eq:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "subspace S" "subspace T"
shows "S homeomorphic T \<longleftrightarrow> dim S = dim T"
@@ -2765,7 +2765,7 @@
by (simp add: assms homeomorphic_subspaces)
qed
-lemma%unimportant homeomorphic_affine_sets_eq:
+lemma homeomorphic_affine_sets_eq:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "affine S" "affine T"
shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
@@ -2783,19 +2783,19 @@
by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
qed
-lemma%unimportant homeomorphic_hyperplanes_eq:
+lemma homeomorphic_hyperplanes_eq:
fixes a :: "'a::euclidean_space" and c :: "'b::euclidean_space"
assumes "a \<noteq> 0" "c \<noteq> 0"
shows "({x. a \<bullet> x = b} homeomorphic {x. c \<bullet> x = d} \<longleftrightarrow> DIM('a) = DIM('b))"
apply (auto simp: homeomorphic_affine_sets_eq affine_hyperplane assms)
by (metis DIM_positive Suc_pred)
-lemma%unimportant homeomorphic_UNIV_UNIV:
+lemma homeomorphic_UNIV_UNIV:
shows "(UNIV::'a set) homeomorphic (UNIV::'b set) \<longleftrightarrow>
DIM('a::euclidean_space) = DIM('b::euclidean_space)"
by (simp add: homeomorphic_subspaces_eq)
-lemma%unimportant simply_connected_sphere_gen:
+lemma simply_connected_sphere_gen:
assumes "convex S" "bounded S" and 3: "3 \<le> aff_dim S"
shows "simply_connected(rel_frontier S)"
proof -
@@ -2819,16 +2819,16 @@
qed
qed
-subsection%important\<open>more invariance of domain\<close>
-
-proposition%important invariance_of_domain_sphere_affine_set_gen:
+subsection%important\<open>more invariance of domain\<close>(*FIX ME title? *)
+
+proposition invariance_of_domain_sphere_affine_set_gen:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
and U: "bounded U" "convex U"
and "affine T" and affTU: "aff_dim T < aff_dim U"
and ope: "openin (subtopology euclidean (rel_frontier U)) S"
shows "openin (subtopology euclidean T) (f ` S)"
-proof%unimportant (cases "rel_frontier U = {}")
+proof (cases "rel_frontier U = {}")
case True
then show ?thesis
using ope openin_subset by force
@@ -2927,7 +2927,7 @@
qed
-lemma%unimportant invariance_of_domain_sphere_affine_set:
+lemma invariance_of_domain_sphere_affine_set:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
and "r \<noteq> 0" "affine T" and affTU: "aff_dim T < DIM('a)"
@@ -2948,7 +2948,7 @@
qed
qed
-lemma%unimportant no_embedding_sphere_lowdim:
+lemma no_embedding_sphere_lowdim:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes contf: "continuous_on (sphere a r) f" and injf: "inj_on f (sphere a r)" and "r > 0"
shows "DIM('a) \<le> DIM('b)"
@@ -2969,7 +2969,7 @@
using not_less by blast
qed
-lemma%unimportant simply_connected_sphere:
+lemma simply_connected_sphere:
fixes a :: "'a::euclidean_space"
assumes "3 \<le> DIM('a)"
shows "simply_connected(sphere a r)"
@@ -2986,7 +2986,7 @@
by (simp add: aff_dim_cball)
qed
-lemma%unimportant simply_connected_sphere_eq:
+lemma simply_connected_sphere_eq:
fixes a :: "'a::euclidean_space"
shows "simply_connected(sphere a r) \<longleftrightarrow> 3 \<le> DIM('a) \<or> r \<le> 0" (is "?lhs = ?rhs")
proof (cases "r \<le> 0")
@@ -3029,7 +3029,7 @@
qed
-lemma%unimportant simply_connected_punctured_universe_eq:
+lemma simply_connected_punctured_universe_eq:
fixes a :: "'a::euclidean_space"
shows "simply_connected(- {a}) \<longleftrightarrow> 3 \<le> DIM('a)"
proof -
@@ -3047,17 +3047,17 @@
finally show ?thesis .
qed
-lemma%unimportant not_simply_connected_circle:
+lemma not_simply_connected_circle:
fixes a :: complex
shows "0 < r \<Longrightarrow> \<not> simply_connected(sphere a r)"
by (simp add: simply_connected_sphere_eq)
-proposition%important simply_connected_punctured_convex:
+proposition simply_connected_punctured_convex:
fixes a :: "'a::euclidean_space"
assumes "convex S" and 3: "3 \<le> aff_dim S"
shows "simply_connected(S - {a})"
-proof%unimportant (cases "a \<in> rel_interior S")
+proof (cases "a \<in> rel_interior S")
case True
then obtain e where "a \<in> S" "0 < e" and e: "cball a e \<inter> affine hull S \<subseteq> S"
by (auto simp: rel_interior_cball)
@@ -3096,11 +3096,11 @@
by (meson Diff_subset closure_subset subset_trans)
qed
-corollary%important simply_connected_punctured_universe:
+corollary simply_connected_punctured_universe:
fixes a :: "'a::euclidean_space"
assumes "3 \<le> DIM('a)"
shows "simply_connected(- {a})"
-proof%unimportant -
+proof -
have [simp]: "affine hull cball a 1 = UNIV"
apply auto
by (metis UNIV_I aff_dim_cball aff_dim_lt_full zero_less_one not_less_iff_gr_or_eq)
@@ -3116,10 +3116,10 @@
subsection%important\<open>The power, squaring and exponential functions as covering maps\<close>
-proposition%important covering_space_power_punctured_plane:
+proposition covering_space_power_punctured_plane:
assumes "0 < n"
shows "covering_space (- {0}) (\<lambda>z::complex. z^n) (- {0})"
-proof%unimportant -
+proof -
consider "n = 1" | "2 \<le> n" using assms by linarith
then obtain e where "0 < e"
and e: "\<And>w z. cmod(w - z) < e * cmod z \<Longrightarrow> (w^n = z^n \<longleftrightarrow> w = z)"
@@ -3367,14 +3367,14 @@
done
qed
-corollary%important covering_space_square_punctured_plane:
+corollary covering_space_square_punctured_plane:
"covering_space (- {0}) (\<lambda>z::complex. z^2) (- {0})"
by%unimportant (simp add: covering_space_power_punctured_plane)
-proposition%important covering_space_exp_punctured_plane:
+proposition covering_space_exp_punctured_plane:
"covering_space UNIV (\<lambda>z::complex. exp z) (- {0})"
-proof%unimportant (simp add: covering_space_def, intro conjI ballI)
+proof (simp add: covering_space_def, intro conjI ballI)
show "continuous_on UNIV (\<lambda>z::complex. exp z)"
by (rule continuous_on_exp [OF continuous_on_id])
show "range exp = - {0::complex}"
@@ -3487,9 +3487,9 @@
qed
-subsection%important\<open>Hence the Borsukian results about mappings into circles\<close>
-
-lemma%unimportant inessential_eq_continuous_logarithm:
+subsection%important\<open>Hence the Borsukian results about mappings into circles\<close>(*FIX ME title *)
+
+lemma inessential_eq_continuous_logarithm:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
(\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x)))"
@@ -3513,7 +3513,7 @@
by (simp add: f homotopic_with_eq)
qed
-corollary%important inessential_imp_continuous_logarithm_circle:
+corollary inessential_imp_continuous_logarithm_circle:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
assumes "homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)"
obtains g where "continuous_on S g" and "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
@@ -3525,7 +3525,7 @@
qed
-lemma%unimportant inessential_eq_continuous_logarithm_circle:
+lemma inessential_eq_continuous_logarithm_circle:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)) \<longleftrightarrow>
(\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x))))"
@@ -3565,12 +3565,12 @@
by (simp add: homotopic_with_eq)
qed
-lemma%important homotopic_with_sphere_times:
+proposition homotopic_with_sphere_times:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
assumes hom: "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g" and conth: "continuous_on S h"
and hin: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> sphere 0 1"
shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x * h x) (\<lambda>x. g x * h x)"
-proof%unimportant -
+proof -
obtain k where contk: "continuous_on ({0..1::real} \<times> S) k"
and kim: "k ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
and k0: "\<And>x. k(0, x) = f x"
@@ -3585,14 +3585,13 @@
done
qed
-
-lemma%important homotopic_circlemaps_divide:
+proposition homotopic_circlemaps_divide:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c))"
-proof%unimportant -
+proof -
have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
if "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)" for c
proof -
@@ -3646,7 +3645,7 @@
text\<open>Many similar proofs below.\<close>
-lemma%unimportant upper_hemicontinuous:
+lemma upper_hemicontinuous:
assumes "\<And>x. x \<in> S \<Longrightarrow> f x \<subseteq> T"
shows "((\<forall>U. openin (subtopology euclidean T) U
\<longrightarrow> openin (subtopology euclidean S) {x \<in> S. f x \<subseteq> U}) \<longleftrightarrow>
@@ -3677,7 +3676,7 @@
by (simp add: openin_closedin_eq)
qed
-lemma%unimportant lower_hemicontinuous:
+lemma lower_hemicontinuous:
assumes "\<And>x. x \<in> S \<Longrightarrow> f x \<subseteq> T"
shows "((\<forall>U. closedin (subtopology euclidean T) U
\<longrightarrow> closedin (subtopology euclidean S) {x \<in> S. f x \<subseteq> U}) \<longleftrightarrow>
@@ -3708,7 +3707,7 @@
by (simp add: openin_closedin_eq)
qed
-lemma%unimportant open_map_iff_lower_hemicontinuous_preimage:
+lemma open_map_iff_lower_hemicontinuous_preimage:
assumes "f ` S \<subseteq> T"
shows "((\<forall>U. openin (subtopology euclidean S) U
\<longrightarrow> openin (subtopology euclidean T) (f ` U)) \<longleftrightarrow>
@@ -3739,7 +3738,7 @@
using assms openin_imp_subset [OF opeSU] by (force simp: openin_closedin_eq)
qed
-lemma%unimportant closed_map_iff_upper_hemicontinuous_preimage:
+lemma closed_map_iff_upper_hemicontinuous_preimage:
assumes "f ` S \<subseteq> T"
shows "((\<forall>U. closedin (subtopology euclidean S) U
\<longrightarrow> closedin (subtopology euclidean T) (f ` U)) \<longleftrightarrow>
@@ -3770,7 +3769,7 @@
by (simp add: openin_closedin_eq)
qed
-proposition%important upper_lower_hemicontinuous_explicit:
+proposition upper_lower_hemicontinuous_explicit:
fixes T :: "('b::{real_normed_vector,heine_borel}) set"
assumes fST: "\<And>x. x \<in> S \<Longrightarrow> f x \<subseteq> T"
and ope: "\<And>U. openin (subtopology euclidean T) U
@@ -3782,7 +3781,7 @@
"\<And>x'. \<lbrakk>x' \<in> S; dist x x' < d\<rbrakk>
\<Longrightarrow> (\<forall>y \<in> f x. \<exists>y'. y' \<in> f x' \<and> dist y y' < e) \<and>
(\<forall>y' \<in> f x'. \<exists>y. y \<in> f x \<and> dist y' y < e)"
-proof%unimportant -
+proof -
have "openin (subtopology euclidean T) (T \<inter> (\<Union>a\<in>f x. \<Union>b\<in>ball 0 e. {a + b}))"
by (auto simp: open_sums openin_open_Int)
with ope have "openin (subtopology euclidean S)
@@ -3843,11 +3842,11 @@
subsection%important\<open>Complex logs exist on various "well-behaved" sets\<close>
-lemma%important continuous_logarithm_on_contractible:
+lemma continuous_logarithm_on_contractible:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
assumes "continuous_on S f" "contractible S" "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
obtains g where "continuous_on S g" "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
-proof%unimportant -
+proof -
obtain c where hom: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>x. c)"
using nullhomotopic_from_contractible assms
by (metis imageE subset_Compl_singleton)
@@ -3855,27 +3854,27 @@
by (metis inessential_eq_continuous_logarithm that)
qed
-lemma%important continuous_logarithm_on_simply_connected:
+lemma continuous_logarithm_on_simply_connected:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
assumes contf: "continuous_on S f" and S: "simply_connected S" "locally path_connected S"
and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
obtains g where "continuous_on S g" "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
- using%unimportant covering_space_lift [OF covering_space_exp_punctured_plane S contf]
- by%unimportant (metis (full_types) f imageE subset_Compl_singleton)
-
-lemma%unimportant continuous_logarithm_on_cball:
+ using covering_space_lift [OF covering_space_exp_punctured_plane S contf]
+ by (metis (full_types) f imageE subset_Compl_singleton)
+
+lemma continuous_logarithm_on_cball:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
assumes "continuous_on (cball a r) f" and "\<And>z. z \<in> cball a r \<Longrightarrow> f z \<noteq> 0"
obtains h where "continuous_on (cball a r) h" "\<And>z. z \<in> cball a r \<Longrightarrow> f z = exp(h z)"
using assms continuous_logarithm_on_contractible convex_imp_contractible by blast
-lemma%unimportant continuous_logarithm_on_ball:
+lemma continuous_logarithm_on_ball:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
assumes "continuous_on (ball a r) f" and "\<And>z. z \<in> ball a r \<Longrightarrow> f z \<noteq> 0"
obtains h where "continuous_on (ball a r) h" "\<And>z. z \<in> ball a r \<Longrightarrow> f z = exp(h z)"
using assms continuous_logarithm_on_contractible convex_imp_contractible by blast
-lemma%unimportant continuous_sqrt_on_contractible:
+lemma continuous_sqrt_on_contractible:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
assumes "continuous_on S f" "contractible S"
and "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
@@ -3892,7 +3891,7 @@
qed
qed
-lemma%unimportant continuous_sqrt_on_simply_connected:
+lemma continuous_sqrt_on_simply_connected:
fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
assumes contf: "continuous_on S f" and S: "simply_connected S" "locally path_connected S"
and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
@@ -3912,12 +3911,12 @@
subsection%important\<open>Another simple case where sphere maps are nullhomotopic\<close>
-lemma%important inessential_spheremap_2_aux:
+lemma inessential_spheremap_2_aux:
fixes f :: "'a::euclidean_space \<Rightarrow> complex"
assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f"
and fim: "f `(sphere a r) \<subseteq> (sphere 0 1)"
obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) f (\<lambda>x. c)"
-proof%unimportant -
+proof -
obtain g where contg: "continuous_on (sphere a r) g"
and feq: "\<And>x. x \<in> sphere a r \<Longrightarrow> f x = exp(g x)"
proof (rule continuous_logarithm_on_simply_connected [OF contf])
@@ -3939,12 +3938,12 @@
by metis
qed
-lemma%important inessential_spheremap_2:
+lemma inessential_spheremap_2:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2"
and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \<subseteq> (sphere b s)"
obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
-proof%unimportant (cases "s \<le> 0")
+proof (cases "s \<le> 0")
case True
then show ?thesis
using contf contractible_sphere fim nullhomotopic_into_contractible that by blast
@@ -3978,12 +3977,12 @@
subsection%important\<open>Holomorphic logarithms and square roots\<close>
-lemma%important contractible_imp_holomorphic_log:
+lemma contractible_imp_holomorphic_log:
assumes holf: "f holomorphic_on S"
and S: "contractible S"
and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
obtains g where "g holomorphic_on S" "\<And>z. z \<in> S \<Longrightarrow> f z = exp(g z)"
-proof%unimportant -
+proof -
have contf: "continuous_on S f"
by (simp add: holf holomorphic_on_imp_continuous_on)
obtain g where contg: "continuous_on S g" and feq: "\<And>x. x \<in> S \<Longrightarrow> f x = exp (g x)"
@@ -4026,12 +4025,12 @@
qed
(*Identical proofs*)
-lemma%important simply_connected_imp_holomorphic_log:
+lemma simply_connected_imp_holomorphic_log:
assumes holf: "f holomorphic_on S"
and S: "simply_connected S" "locally path_connected S"
and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
obtains g where "g holomorphic_on S" "\<And>z. z \<in> S \<Longrightarrow> f z = exp(g z)"
-proof%unimportant -
+proof -
have contf: "continuous_on S f"
by (simp add: holf holomorphic_on_imp_continuous_on)
obtain g where contg: "continuous_on S g" and feq: "\<And>x. x \<in> S \<Longrightarrow> f x = exp (g x)"
@@ -4074,7 +4073,7 @@
qed
-lemma%unimportant contractible_imp_holomorphic_sqrt:
+lemma contractible_imp_holomorphic_sqrt:
assumes holf: "f holomorphic_on S"
and S: "contractible S"
and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
@@ -4092,7 +4091,7 @@
qed
qed
-lemma%unimportant simply_connected_imp_holomorphic_sqrt:
+lemma simply_connected_imp_holomorphic_sqrt:
assumes holf: "f holomorphic_on S"
and S: "simply_connected S" "locally path_connected S"
and fnz: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
@@ -4112,11 +4111,11 @@
text\<open> Related theorems about holomorphic inverse cosines.\<close>
-lemma%important contractible_imp_holomorphic_arccos:
+lemma contractible_imp_holomorphic_arccos:
assumes holf: "f holomorphic_on S" and S: "contractible S"
and non1: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1"
obtains g where "g holomorphic_on S" "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)"
-proof%unimportant -
+proof -
have hol1f: "(\<lambda>z. 1 - f z ^ 2) holomorphic_on S"
by (intro holomorphic_intros holf)
obtain g where holg: "g holomorphic_on S" and eq: "\<And>z. z \<in> S \<Longrightarrow> 1 - (f z)\<^sup>2 = (g z)\<^sup>2"
@@ -4150,11 +4149,11 @@
qed
-lemma%important contractible_imp_holomorphic_arccos_bounded:
+lemma contractible_imp_holomorphic_arccos_bounded:
assumes holf: "f holomorphic_on S" and S: "contractible S" and "a \<in> S"
and non1: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1"
obtains g where "g holomorphic_on S" "norm(g a) \<le> pi + norm(f a)" "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)"
-proof%unimportant -
+proof -
obtain g where holg: "g holomorphic_on S" and feq: "\<And>z. z \<in> S \<Longrightarrow> f z = cos (g z)"
using contractible_imp_holomorphic_arccos [OF holf S non1] by blast
obtain b where "cos b = f a" "norm b \<le> pi + norm (f a)"
@@ -4200,11 +4199,11 @@
\<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
\<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (- {0}) f (\<lambda>x. a))"
-lemma%important Borsukian_retraction_gen:
+lemma Borsukian_retraction_gen:
assumes "Borsukian S" "continuous_on S h" "h ` S = T"
"continuous_on T k" "k ` T \<subseteq> S" "\<And>y. y \<in> T \<Longrightarrow> h(k y) = y"
shows "Borsukian T"
-proof%unimportant -
+proof -
interpret R: Retracts S h T k
using assms by (simp add: Retracts.intro)
show ?thesis
@@ -4214,42 +4213,42 @@
done
qed
-lemma%unimportant retract_of_Borsukian: "\<lbrakk>Borsukian T; S retract_of T\<rbrakk> \<Longrightarrow> Borsukian S"
+lemma retract_of_Borsukian: "\<lbrakk>Borsukian T; S retract_of T\<rbrakk> \<Longrightarrow> Borsukian S"
apply (auto simp: retract_of_def retraction_def)
apply (erule (1) Borsukian_retraction_gen)
apply (meson retraction retraction_def)
apply (auto simp: continuous_on_id)
done
-lemma%unimportant homeomorphic_Borsukian: "\<lbrakk>Borsukian S; S homeomorphic T\<rbrakk> \<Longrightarrow> Borsukian T"
+lemma homeomorphic_Borsukian: "\<lbrakk>Borsukian S; S homeomorphic T\<rbrakk> \<Longrightarrow> Borsukian T"
using Borsukian_retraction_gen order_refl
by (fastforce simp add: homeomorphism_def homeomorphic_def)
-lemma%unimportant homeomorphic_Borsukian_eq:
+lemma homeomorphic_Borsukian_eq:
"S homeomorphic T \<Longrightarrow> Borsukian S \<longleftrightarrow> Borsukian T"
by (meson homeomorphic_Borsukian homeomorphic_sym)
-lemma%unimportant Borsukian_translation:
+lemma Borsukian_translation:
fixes S :: "'a::real_normed_vector set"
shows "Borsukian (image (\<lambda>x. a + x) S) \<longleftrightarrow> Borsukian S"
apply (rule homeomorphic_Borsukian_eq)
using homeomorphic_translation homeomorphic_sym by blast
-lemma%unimportant Borsukian_injective_linear_image:
+lemma Borsukian_injective_linear_image:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "linear f" "inj f"
shows "Borsukian(f ` S) \<longleftrightarrow> Borsukian S"
apply (rule homeomorphic_Borsukian_eq)
using assms homeomorphic_sym linear_homeomorphic_image by blast
-lemma%unimportant homotopy_eqv_Borsukianness:
+lemma homotopy_eqv_Borsukianness:
fixes S :: "'a::real_normed_vector set"
and T :: "'b::real_normed_vector set"
assumes "S homotopy_eqv T"
shows "(Borsukian S \<longleftrightarrow> Borsukian T)"
by (meson Borsukian_def assms homotopy_eqv_cohomotopic_triviality_null)
-lemma%unimportant Borsukian_alt:
+lemma Borsukian_alt:
fixes S :: "'a::real_normed_vector set"
shows
"Borsukian S \<longleftrightarrow>
@@ -4259,20 +4258,20 @@
unfolding Borsukian_def homotopic_triviality
by (simp add: path_connected_punctured_universe)
-lemma%unimportant Borsukian_continuous_logarithm:
+lemma Borsukian_continuous_logarithm:
fixes S :: "'a::real_normed_vector set"
shows "Borsukian S \<longleftrightarrow>
(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
\<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))))"
by (simp add: Borsukian_def inessential_eq_continuous_logarithm)
-lemma%important Borsukian_continuous_logarithm_circle:
+lemma Borsukian_continuous_logarithm_circle:
fixes S :: "'a::real_normed_vector set"
shows "Borsukian S \<longleftrightarrow>
(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
\<longrightarrow> (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x))))"
(is "?lhs = ?rhs")
-proof%unimportant
+proof
assume ?lhs then show ?rhs
by (force simp: Borsukian_continuous_logarithm)
next
@@ -4302,13 +4301,13 @@
qed
-lemma%important Borsukian_continuous_logarithm_circle_real:
+lemma Borsukian_continuous_logarithm_circle_real:
fixes S :: "'a::real_normed_vector set"
shows "Borsukian S \<longleftrightarrow>
(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
\<longrightarrow> (\<exists>g. continuous_on S (complex_of_real \<circ> g) \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x)))))"
(is "?lhs = ?rhs")
-proof%unimportant
+proof
assume LHS: ?lhs
show ?rhs
proof (clarify)
@@ -4335,52 +4334,52 @@
qed
qed
-lemma%unimportant Borsukian_circle:
+lemma Borsukian_circle:
fixes S :: "'a::real_normed_vector set"
shows "Borsukian S \<longleftrightarrow>
(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
\<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (sphere (0::complex) 1) f (\<lambda>x. a)))"
by (simp add: inessential_eq_continuous_logarithm_circle Borsukian_continuous_logarithm_circle_real)
-lemma%unimportant contractible_imp_Borsukian: "contractible S \<Longrightarrow> Borsukian S"
+lemma contractible_imp_Borsukian: "contractible S \<Longrightarrow> Borsukian S"
by (meson Borsukian_def nullhomotopic_from_contractible)
-lemma%unimportant simply_connected_imp_Borsukian:
+lemma simply_connected_imp_Borsukian:
fixes S :: "'a::real_normed_vector set"
shows "\<lbrakk>simply_connected S; locally path_connected S\<rbrakk> \<Longrightarrow> Borsukian S"
apply (simp add: Borsukian_continuous_logarithm)
by (metis (no_types, lifting) continuous_logarithm_on_simply_connected image_iff)
-lemma%unimportant starlike_imp_Borsukian:
+lemma starlike_imp_Borsukian:
fixes S :: "'a::real_normed_vector set"
shows "starlike S \<Longrightarrow> Borsukian S"
by (simp add: contractible_imp_Borsukian starlike_imp_contractible)
-lemma%unimportant Borsukian_empty: "Borsukian {}"
+lemma Borsukian_empty: "Borsukian {}"
by (auto simp: contractible_imp_Borsukian)
-lemma%unimportant Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)"
+lemma Borsukian_UNIV: "Borsukian (UNIV :: 'a::real_normed_vector set)"
by (auto simp: contractible_imp_Borsukian)
-lemma%unimportant convex_imp_Borsukian:
+lemma convex_imp_Borsukian:
fixes S :: "'a::real_normed_vector set"
shows "convex S \<Longrightarrow> Borsukian S"
by (meson Borsukian_def convex_imp_contractible nullhomotopic_from_contractible)
-lemma%unimportant Borsukian_sphere:
+proposition Borsukian_sphere:
fixes a :: "'a::euclidean_space"
shows "3 \<le> DIM('a) \<Longrightarrow> Borsukian (sphere a r)"
apply (rule simply_connected_imp_Borsukian)
using simply_connected_sphere apply blast
using ENR_imp_locally_path_connected ENR_sphere by blast
-lemma%important Borsukian_open_Un:
+proposition Borsukian_open_Un:
fixes S :: "'a::real_normed_vector set"
assumes opeS: "openin (subtopology euclidean (S \<union> T)) S"
and opeT: "openin (subtopology euclidean (S \<union> T)) T"
and BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S \<inter> T)"
shows "Borsukian(S \<union> T)"
-proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm)
+proof (clarsimp simp add: Borsukian_continuous_logarithm)
fix f :: "'a \<Rightarrow> complex"
assume contf: "continuous_on (S \<union> T) f" and 0: "0 \<notin> f ` (S \<union> T)"
then have contfS: "continuous_on S f" and contfT: "continuous_on T f"
@@ -4444,13 +4443,13 @@
qed
text\<open>The proof is a duplicate of that of \<open>Borsukian_open_Un\<close>.\<close>
-lemma%important Borsukian_closed_Un:
+lemma Borsukian_closed_Un:
fixes S :: "'a::real_normed_vector set"
assumes cloS: "closedin (subtopology euclidean (S \<union> T)) S"
and cloT: "closedin (subtopology euclidean (S \<union> T)) T"
and BS: "Borsukian S" and BT: "Borsukian T" and ST: "connected(S \<inter> T)"
shows "Borsukian(S \<union> T)"
-proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm)
+proof (clarsimp simp add: Borsukian_continuous_logarithm)
fix f :: "'a \<Rightarrow> complex"
assume contf: "continuous_on (S \<union> T) f" and 0: "0 \<notin> f ` (S \<union> T)"
then have contfS: "continuous_on S f" and contfT: "continuous_on T f"
@@ -4513,18 +4512,18 @@
qed
qed
-lemma%unimportant Borsukian_separation_compact:
+lemma Borsukian_separation_compact:
fixes S :: "complex set"
assumes "compact S"
shows "Borsukian S \<longleftrightarrow> connected(- S)"
by (simp add: Borsuk_separation_theorem Borsukian_circle assms)
-lemma%important Borsukian_monotone_image_compact:
+lemma Borsukian_monotone_image_compact:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T"
and "compact S" and conn: "\<And>y. y \<in> T \<Longrightarrow> connected {x. x \<in> S \<and> f x = y}"
shows "Borsukian T"
-proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm)
+proof (clarsimp simp add: Borsukian_continuous_logarithm)
fix g :: "'b \<Rightarrow> complex"
assume contg: "continuous_on T g" and 0: "0 \<notin> g ` T"
have "continuous_on S (g \<circ> f)"
@@ -4584,13 +4583,13 @@
qed
-lemma%important Borsukian_open_map_image_compact:
+lemma Borsukian_open_map_image_compact:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "Borsukian S" and contf: "continuous_on S f" and fim: "f ` S = T" and "compact S"
and ope: "\<And>U. openin (subtopology euclidean S) U
\<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
shows "Borsukian T"
-proof%unimportant (clarsimp simp add: Borsukian_continuous_logarithm_circle_real)
+proof (clarsimp simp add: Borsukian_continuous_logarithm_circle_real)
fix g :: "'b \<Rightarrow> complex"
assume contg: "continuous_on T g" and gim: "g ` T \<subseteq> sphere 0 1"
have "continuous_on S (g \<circ> f)"
@@ -4671,12 +4670,12 @@
text\<open>If two points are separated by a closed set, there's a minimal one.\<close>
-proposition%important closed_irreducible_separator:
+proposition closed_irreducible_separator:
fixes a :: "'a::real_normed_vector"
assumes "closed S" and ab: "\<not> connected_component (- S) a b"
obtains T where "T \<subseteq> S" "closed T" "T \<noteq> {}" "\<not> connected_component (- T) a b"
"\<And>U. U \<subset> T \<Longrightarrow> connected_component (- U) a b"
-proof%unimportant (cases "a \<in> S \<or> b \<in> S")
+proof (cases "a \<in> S \<or> b \<in> S")
case True
then show ?thesis
proof
@@ -4779,7 +4778,7 @@
qed
qed
-lemma%unimportant frontier_minimal_separating_closed_pointwise:
+lemma frontier_minimal_separating_closed_pointwise:
fixes S :: "'a::real_normed_vector set"
assumes S: "closed S" "a \<notin> S" and nconn: "\<not> connected_component (- S) a b"
and conn: "\<And>T. \<lbrakk>closed T; T \<subset> S\<rbrakk> \<Longrightarrow> connected_component (- T) a b"
@@ -4816,21 +4815,21 @@
closedin (subtopology euclidean U) S \<and> closedin (subtopology euclidean U) T
\<longrightarrow> connected (S \<inter> T)"
-lemma%unimportant unicoherentI [intro?]:
+lemma unicoherentI [intro?]:
assumes "\<And>S T. \<lbrakk>connected S; connected T; U = S \<union> T; closedin (subtopology euclidean U) S; closedin (subtopology euclidean U) T\<rbrakk>
\<Longrightarrow> connected (S \<inter> T)"
shows "unicoherent U"
using assms unfolding unicoherent_def by blast
-lemma%unimportant unicoherentD:
+lemma unicoherentD:
assumes "unicoherent U" "connected S" "connected T" "U = S \<union> T" "closedin (subtopology euclidean U) S" "closedin (subtopology euclidean U) T"
shows "connected (S \<inter> T)"
using assms unfolding unicoherent_def by blast
-lemma%important homeomorphic_unicoherent:
+proposition homeomorphic_unicoherent:
assumes ST: "S homeomorphic T" and S: "unicoherent S"
shows "unicoherent T"
-proof%unimportant -
+proof -
obtain f g where gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x" and fim: "T = f ` S" and gfim: "g ` f ` S = S"
and contf: "continuous_on S f" and contg: "continuous_on (f ` S) g"
using ST by (auto simp: homeomorphic_def homeomorphism_def)
@@ -4871,24 +4870,24 @@
qed
-lemma%unimportant homeomorphic_unicoherent_eq:
+lemma homeomorphic_unicoherent_eq:
"S homeomorphic T \<Longrightarrow> (unicoherent S \<longleftrightarrow> unicoherent T)"
by (meson homeomorphic_sym homeomorphic_unicoherent)
-lemma%unimportant unicoherent_translation:
+lemma unicoherent_translation:
fixes S :: "'a::real_normed_vector set"
shows
"unicoherent (image (\<lambda>x. a + x) S) \<longleftrightarrow> unicoherent S"
using homeomorphic_translation homeomorphic_unicoherent_eq by blast
-lemma%unimportant unicoherent_injective_linear_image:
+lemma unicoherent_injective_linear_image:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "linear f" "inj f"
shows "(unicoherent(f ` S) \<longleftrightarrow> unicoherent S)"
using assms homeomorphic_unicoherent_eq linear_homeomorphic_image by blast
-lemma%unimportant Borsukian_imp_unicoherent:
+lemma Borsukian_imp_unicoherent:
fixes U :: "'a::euclidean_space set"
assumes "Borsukian U" shows "unicoherent U"
unfolding unicoherent_def
@@ -4998,27 +4997,27 @@
qed
-corollary%important contractible_imp_unicoherent:
+corollary contractible_imp_unicoherent:
fixes U :: "'a::euclidean_space set"
assumes "contractible U" shows "unicoherent U"
by%unimportant (simp add: Borsukian_imp_unicoherent assms contractible_imp_Borsukian)
-corollary%important convex_imp_unicoherent:
+corollary convex_imp_unicoherent:
fixes U :: "'a::euclidean_space set"
assumes "convex U" shows "unicoherent U"
by%unimportant (simp add: Borsukian_imp_unicoherent assms convex_imp_Borsukian)
text\<open>If the type class constraint can be relaxed, I don't know how!\<close>
-corollary%important unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)"
+corollary unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)"
by%unimportant (simp add: convex_imp_unicoherent)
-lemma%important unicoherent_monotone_image_compact:
+lemma unicoherent_monotone_image_compact:
fixes T :: "'b :: t2_space set"
assumes S: "unicoherent S" "compact S" and contf: "continuous_on S f" and fim: "f ` S = T"
and conn: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
shows "unicoherent T"
-proof%unimportant
+proof
fix U V
assume UV: "connected U" "connected V" "T = U \<union> V"
and cloU: "closedin (subtopology euclidean T) U"
@@ -5054,7 +5053,7 @@
subsection%important\<open>Several common variants of unicoherence\<close>
-lemma%unimportant connected_frontier_simple:
+lemma connected_frontier_simple:
fixes S :: "'a :: euclidean_space set"
assumes "connected S" "connected(- S)" shows "connected(frontier S)"
unfolding frontier_closures
@@ -5062,18 +5061,18 @@
apply (simp_all add: assms connected_imp_connected_closure)
by (simp add: closure_def)
-lemma%unimportant connected_frontier_component_complement:
+lemma connected_frontier_component_complement:
fixes S :: "'a :: euclidean_space set"
assumes "connected S" and C: "C \<in> components(- S)" shows "connected(frontier C)"
apply (rule connected_frontier_simple)
using C in_components_connected apply blast
by (metis Compl_eq_Diff_UNIV connected_UNIV assms top_greatest component_complement_connected)
-lemma%important connected_frontier_disjoint:
+lemma connected_frontier_disjoint:
fixes S :: "'a :: euclidean_space set"
assumes "connected S" "connected T" "disjnt S T" and ST: "frontier S \<subseteq> frontier T"
shows "connected(frontier S)"
-proof%unimportant (cases "S = UNIV")
+proof (cases "S = UNIV")
case True then show ?thesis
by simp
next
@@ -5107,11 +5106,11 @@
subsection%important\<open>Some separation results\<close>
-lemma%important separation_by_component_closed_pointwise:
+lemma separation_by_component_closed_pointwise:
fixes S :: "'a :: euclidean_space set"
assumes "closed S" "\<not> connected_component (- S) a b"
obtains C where "C \<in> components S" "\<not> connected_component(- C) a b"
-proof%unimportant (cases "a \<in> S \<or> b \<in> S")
+proof (cases "a \<in> S \<or> b \<in> S")
case True
then show ?thesis
using connected_component_in componentsI that by fastforce
@@ -5144,11 +5143,11 @@
qed
-lemma%important separation_by_component_closed:
+lemma separation_by_component_closed:
fixes S :: "'a :: euclidean_space set"
assumes "closed S" "\<not> connected(- S)"
obtains C where "C \<in> components S" "\<not> connected(- C)"
-proof%unimportant -
+proof -
obtain x y where "closed S" "x \<notin> S" "y \<notin> S" and "\<not> connected_component (- S) x y"
using assms by (auto simp: connected_iff_connected_component)
then obtain C where "C \<in> components S" "\<not> connected_component(- C) x y"
@@ -5158,12 +5157,12 @@
by (metis Compl_iff \<open>C \<in> components S\<close> \<open>x \<notin> S\<close> \<open>y \<notin> S\<close> connected_component_eq connected_component_eq_eq connected_iff_connected_component that)
qed
-lemma%important separation_by_Un_closed_pointwise:
+lemma separation_by_Un_closed_pointwise:
fixes S :: "'a :: euclidean_space set"
assumes ST: "closed S" "closed T" "S \<inter> T = {}"
and conS: "connected_component (- S) a b" and conT: "connected_component (- T) a b"
shows "connected_component (- (S \<union> T)) a b"
-proof%unimportant (rule ccontr)
+proof (rule ccontr)
have "a \<notin> S" "b \<notin> S" "a \<notin> T" "b \<notin> T"
using conS conT connected_component_in by auto
assume "\<not> connected_component (- (S \<union> T)) a b"
@@ -5182,14 +5181,14 @@
by (meson Compl_anti_mono C conS conT connected_component_of_subset)
qed
-lemma%unimportant separation_by_Un_closed:
+lemma separation_by_Un_closed:
fixes S :: "'a :: euclidean_space set"
assumes ST: "closed S" "closed T" "S \<inter> T = {}" and conS: "connected(- S)" and conT: "connected(- T)"
shows "connected(- (S \<union> T))"
using assms separation_by_Un_closed_pointwise
by (fastforce simp add: connected_iff_connected_component)
-lemma%unimportant open_unicoherent_UNIV:
+lemma open_unicoherent_UNIV:
fixes S :: "'a :: euclidean_space set"
assumes "open S" "open T" "connected S" "connected T" "S \<union> T = UNIV"
shows "connected(S \<inter> T)"
@@ -5200,7 +5199,7 @@
by simp
qed
-lemma%unimportant separation_by_component_open_aux:
+lemma separation_by_component_open_aux:
fixes S :: "'a :: euclidean_space set"
assumes ST: "closed S" "closed T" "S \<inter> T = {}"
and "S \<noteq> {}" "T \<noteq> {}"
@@ -5280,11 +5279,11 @@
qed
-lemma%important separation_by_component_open:
+proposition separation_by_component_open:
fixes S :: "'a :: euclidean_space set"
assumes "open S" and non: "\<not> connected(- S)"
obtains C where "C \<in> components S" "\<not> connected(- C)"
-proof%unimportant -
+proof -
obtain T U
where "closed T" "closed U" and TU: "T \<union> U = - S" "T \<inter> U = {}" "T \<noteq> {}" "U \<noteq> {}"
using assms by (auto simp: connected_closed_set closed_def)
@@ -5307,18 +5306,18 @@
qed
qed
-lemma%unimportant separation_by_Un_open:
+lemma separation_by_Un_open:
fixes S :: "'a :: euclidean_space set"
assumes "open S" "open T" "S \<inter> T = {}" and cS: "connected(-S)" and cT: "connected(-T)"
shows "connected(- (S \<union> T))"
using assms unicoherent_UNIV unfolding unicoherent_def by force
-lemma%important nonseparation_by_component_eq:
+lemma nonseparation_by_component_eq:
fixes S :: "'a :: euclidean_space set"
assumes "open S \<or> closed S"
shows "((\<forall>C \<in> components S. connected(-C)) \<longleftrightarrow> connected(- S))" (is "?lhs = ?rhs")
-proof%unimportant
+proof
assume ?lhs with assms show ?rhs
by (meson separation_by_component_closed separation_by_component_open)
next
@@ -5328,13 +5327,13 @@
text\<open>Another interesting equivalent of an inessential mapping into C-{0}\<close>
-proposition%important inessential_eq_extensible:
+proposition inessential_eq_extensible:
fixes f :: "'a::euclidean_space \<Rightarrow> complex"
assumes "closed S"
shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
(\<exists>g. continuous_on UNIV g \<and> (\<forall>x \<in> S. g x = f x) \<and> (\<forall>x. g x \<noteq> 0))"
(is "?lhs = ?rhs")
-proof%unimportant
+proof
assume ?lhs
then obtain a where a: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)" ..
show ?rhs
@@ -5394,14 +5393,14 @@
by (simp add: inessential_eq_continuous_logarithm)
qed
-lemma%important inessential_on_clopen_Union:
+lemma inessential_on_clopen_Union:
fixes \<F> :: "'a::euclidean_space set set"
assumes T: "path_connected T"
and "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
and hom: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)"
obtains a where "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
-proof%unimportant (cases "\<Union>\<F> = {}")
+proof (cases "\<Union>\<F> = {}")
case True
with that show ?thesis
by force
@@ -5442,12 +5441,12 @@
then show ?thesis ..
qed
-lemma%important Janiszewski_dual:
+proposition Janiszewski_dual:
fixes S :: "complex set"
assumes
"compact S" "compact T" "connected S" "connected T" "connected(- (S \<union> T))"
shows "connected(S \<inter> T)"
-proof%unimportant -
+proof -
have ST: "compact (S \<union> T)"
by (simp add: assms compact_Un)
with Borsukian_imp_unicoherent [of "S \<union> T"] ST assms
--- a/src/HOL/Analysis/Great_Picard.thy Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Great_Picard.thy Thu Jan 17 15:50:28 2019 +0000
@@ -9,13 +9,13 @@
subsection\<open>Schottky's theorem\<close>
-lemma%important Schottky_lemma0:
+lemma Schottky_lemma0:
assumes holf: "f holomorphic_on S" and cons: "contractible S" and "a \<in> S"
and f: "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 1 \<and> f z \<noteq> -1"
obtains g where "g holomorphic_on S"
"norm(g a) \<le> 1 + norm(f a) / 3"
"\<And>z. z \<in> S \<Longrightarrow> f z = cos(of_real pi * g z)"
-proof%unimportant -
+proof -
obtain g where holg: "g holomorphic_on S" and g: "norm(g a) \<le> pi + norm(f a)"
and f_eq_cos: "\<And>z. z \<in> S \<Longrightarrow> f z = cos(g z)"
using contractible_imp_holomorphic_arccos_bounded [OF assms]
@@ -38,7 +38,7 @@
qed
-lemma%unimportant Schottky_lemma1:
+lemma Schottky_lemma1:
fixes n::nat
assumes "0 < n"
shows "0 < n + sqrt(real n ^ 2 - 1)"
@@ -54,7 +54,7 @@
qed
-lemma%unimportant Schottky_lemma2:
+lemma Schottky_lemma2:
fixes x::real
assumes "0 \<le> x"
obtains n where "0 < n" "\<bar>x - ln (real n + sqrt ((real n)\<^sup>2 - 1)) / pi\<bar> < 1/2"
@@ -158,12 +158,12 @@
qed
-lemma%important Schottky_lemma3:
+lemma Schottky_lemma3:
fixes z::complex
assumes "z \<in> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (ln(n + sqrt(real n ^ 2 - 1)) / pi)})
\<union> (\<Union>m \<in> Ints. \<Union>n \<in> {0<..}. {Complex m (-ln(n + sqrt(real n ^ 2 - 1)) / pi)})"
shows "cos(pi * cos(pi * z)) = 1 \<or> cos(pi * cos(pi * z)) = -1"
-proof%unimportant -
+proof -
have sqrt2 [simp]: "complex_of_real (sqrt x) * complex_of_real (sqrt x) = x" if "x \<ge> 0" for x::real
by (metis abs_of_nonneg of_real_mult real_sqrt_mult_self that)
have 1: "\<exists>k. exp (\<i> * (of_int m * complex_of_real pi) -
@@ -223,13 +223,13 @@
qed
-theorem%important Schottky:
+theorem Schottky:
assumes holf: "f holomorphic_on cball 0 1"
and nof0: "norm(f 0) \<le> r"
and not01: "\<And>z. z \<in> cball 0 1 \<Longrightarrow> \<not>(f z = 0 \<or> f z = 1)"
and "0 < t" "t < 1" "norm z \<le> t"
shows "norm(f z) \<le> exp(pi * exp(pi * (2 + 2 * r + 12 * t / (1 - t))))"
-proof%unimportant -
+proof -
obtain h where holf: "h holomorphic_on cball 0 1"
and nh0: "norm (h 0) \<le> 1 + norm(2 * f 0 - 1) / 3"
and h: "\<And>z. z \<in> cball 0 1 \<Longrightarrow> 2 * f z - 1 = cos(of_real pi * h z)"
@@ -376,12 +376,12 @@
subsection%important\<open>The Little Picard Theorem\<close>
-lemma%important Landau_Picard:
+proposition Landau_Picard:
obtains R
where "\<And>z. 0 < R z"
"\<And>f. \<lbrakk>f holomorphic_on cball 0 (R(f 0));
\<And>z. norm z \<le> R(f 0) \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1\<rbrakk> \<Longrightarrow> norm(deriv f 0) < 1"
-proof%unimportant -
+proof -
define R where "R \<equiv> \<lambda>z. 3 * exp(pi * exp(pi*(2 + 2 * cmod z + 12)))"
show ?thesis
proof
@@ -436,10 +436,10 @@
qed
qed
-lemma%important little_Picard_01:
+lemma little_Picard_01:
assumes holf: "f holomorphic_on UNIV" and f01: "\<And>z. f z \<noteq> 0 \<and> f z \<noteq> 1"
obtains c where "f = (\<lambda>x. c)"
-proof%unimportant -
+proof -
obtain R
where Rpos: "\<And>z. 0 < R z"
and R: "\<And>h. \<lbrakk>h holomorphic_on cball 0 (R(h 0));
@@ -481,11 +481,11 @@
qed
-theorem%important little_Picard:
+theorem little_Picard:
assumes holf: "f holomorphic_on UNIV"
and "a \<noteq> b" "range f \<inter> {a,b} = {}"
obtains c where "f = (\<lambda>x. c)"
-proof%unimportant -
+proof -
let ?g = "\<lambda>x. 1/(b - a)*(f x - b) + 1"
obtain c where "?g = (\<lambda>x. c)"
proof (rule little_Picard_01)
@@ -505,7 +505,7 @@
text\<open>A couple of little applications of Little Picard\<close>
-lemma%unimportant holomorphic_periodic_fixpoint:
+lemma holomorphic_periodic_fixpoint:
assumes holf: "f holomorphic_on UNIV"
and "p \<noteq> 0" and per: "\<And>z. f(z + p) = f z"
obtains x where "f x = x"
@@ -527,7 +527,7 @@
qed
-lemma%unimportant holomorphic_involution_point:
+lemma holomorphic_involution_point:
assumes holfU: "f holomorphic_on UNIV" and non: "\<And>a. f \<noteq> (\<lambda>x. a + x)"
obtains x where "f(f x) = x"
proof -
@@ -616,7 +616,7 @@
subsection%important\<open>The Arzelà --Ascoli theorem\<close>
-lemma%unimportant subsequence_diagonalization_lemma:
+lemma subsequence_diagonalization_lemma:
fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
assumes sub: "\<And>i r. \<exists>k. strict_mono (k :: nat \<Rightarrow> nat) \<and> P i (r \<circ> k)"
and P_P: "\<And>i r::nat \<Rightarrow> 'a. \<And>k1 k2 N.
@@ -660,7 +660,7 @@
qed
qed
-lemma%unimportant function_convergent_subsequence:
+lemma function_convergent_subsequence:
fixes f :: "[nat,'a] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
assumes "countable S" and M: "\<And>n::nat. \<And>x. x \<in> S \<Longrightarrow> norm(f n x) \<le> M"
obtains k where "strict_mono (k::nat\<Rightarrow>nat)" "\<And>x. x \<in> S \<Longrightarrow> \<exists>l. (\<lambda>n. f (k n) x) \<longlonglongrightarrow> l"
@@ -698,7 +698,7 @@
qed
-theorem%important Arzela_Ascoli:
+theorem Arzela_Ascoli:
fixes \<F> :: "[nat,'a::euclidean_space] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
assumes "compact S"
and M: "\<And>n x. x \<in> S \<Longrightarrow> norm(\<F> n x) \<le> M"
@@ -707,7 +707,7 @@
\<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n y. y \<in> S \<and> norm(x - y) < d \<longrightarrow> norm(\<F> n x - \<F> n y) < e)"
obtains g k where "continuous_on S g" "strict_mono (k :: nat \<Rightarrow> nat)"
"\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<and> x \<in> S \<longrightarrow> norm(\<F>(k n) x - g x) < e"
-proof%unimportant -
+proof -
have UEQ: "\<And>e. 0 < e \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n. \<forall>x \<in> S. \<forall>x' \<in> S. dist x' x < d \<longrightarrow> dist (\<F> n x') (\<F> n x) < e)"
apply (rule compact_uniformly_equicontinuous [OF \<open>compact S\<close>, of "range \<F>"])
using equicont by (force simp: dist_commute dist_norm)+
@@ -795,7 +795,7 @@
holomorphic function, and converges \emph{uniformly} on compact subsets of S.\<close>
-theorem%important Montel:
+theorem Montel:
fixes \<F> :: "[nat,complex] \<Rightarrow> complex"
assumes "open S"
and \<H>: "\<And>h. h \<in> \<H> \<Longrightarrow> h holomorphic_on S"
@@ -805,7 +805,7 @@
where "g holomorphic_on S" "strict_mono (r :: nat \<Rightarrow> nat)"
"\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>n. \<F> (r n) x) \<longlongrightarrow> g x) sequentially"
"\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K (\<F> \<circ> r) g sequentially"
-proof%unimportant -
+proof -
obtain K where comK: "\<And>n. compact(K n)" and KS: "\<And>n::nat. K n \<subseteq> S"
and subK: "\<And>X. \<lbrakk>compact X; X \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. X \<subseteq> K n"
using open_Union_compact_subsets [OF \<open>open S\<close>] by metis
@@ -995,7 +995,7 @@
subsection%important\<open>Some simple but useful cases of Hurwitz's theorem\<close>
-proposition%important Hurwitz_no_zeros:
+proposition Hurwitz_no_zeros:
assumes S: "open S" "connected S"
and holf: "\<And>n::nat. \<F> n holomorphic_on S"
and holg: "g holomorphic_on S"
@@ -1004,7 +1004,7 @@
and nz: "\<And>n z. z \<in> S \<Longrightarrow> \<F> n z \<noteq> 0"
and "z0 \<in> S"
shows "g z0 \<noteq> 0"
-proof%unimportant
+proof
assume g0: "g z0 = 0"
obtain h r m
where "0 < m" "0 < r" and subS: "ball z0 r \<subseteq> S"
@@ -1159,7 +1159,7 @@
ultimately show False using \<open>0 < m\<close> by auto
qed
-corollary%important Hurwitz_injective:
+corollary Hurwitz_injective:
assumes S: "open S" "connected S"
and holf: "\<And>n::nat. \<F> n holomorphic_on S"
and holg: "g holomorphic_on S"
@@ -1167,7 +1167,7 @@
and nonconst: "\<not> g constant_on S"
and inj: "\<And>n. inj_on (\<F> n) S"
shows "inj_on g S"
-proof%unimportant -
+proof -
have False if z12: "z1 \<in> S" "z2 \<in> S" "z1 \<noteq> z2" "g z2 = g z1" for z1 z2
proof -
obtain z0 where "z0 \<in> S" and z0: "g z0 \<noteq> g z2"
@@ -1231,13 +1231,13 @@
subsection%important\<open>The Great Picard theorem\<close>
-lemma%important GPicard1:
+lemma GPicard1:
assumes S: "open S" "connected S" and "w \<in> S" "0 < r" "Y \<subseteq> X"
and holX: "\<And>h. h \<in> X \<Longrightarrow> h holomorphic_on S"
and X01: "\<And>h z. \<lbrakk>h \<in> X; z \<in> S\<rbrakk> \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1"
and r: "\<And>h. h \<in> Y \<Longrightarrow> norm(h w) \<le> r"
obtains B Z where "0 < B" "open Z" "w \<in> Z" "Z \<subseteq> S" "\<And>h z. \<lbrakk>h \<in> Y; z \<in> Z\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
-proof%unimportant -
+proof -
obtain e where "e > 0" and e: "cball w e \<subseteq> S"
using assms open_contains_cball_eq by blast
show ?thesis
@@ -1277,20 +1277,20 @@
qed (use \<open>e > 0\<close> in auto)
qed
-lemma%important GPicard2:
+lemma GPicard2:
assumes "S \<subseteq> T" "connected T" "S \<noteq> {}" "open S" "\<And>x. \<lbrakk>x islimpt S; x \<in> T\<rbrakk> \<Longrightarrow> x \<in> S"
shows "S = T"
- by%unimportant (metis assms open_subset connected_clopen closedin_limpt)
+ by (metis assms open_subset connected_clopen closedin_limpt)
-lemma%important GPicard3:
+lemma GPicard3:
assumes S: "open S" "connected S" "w \<in> S" and "Y \<subseteq> X"
and holX: "\<And>h. h \<in> X \<Longrightarrow> h holomorphic_on S"
and X01: "\<And>h z. \<lbrakk>h \<in> X; z \<in> S\<rbrakk> \<Longrightarrow> h z \<noteq> 0 \<and> h z \<noteq> 1"
and no_hw_le1: "\<And>h. h \<in> Y \<Longrightarrow> norm(h w) \<le> 1"
and "compact K" "K \<subseteq> S"
obtains B where "\<And>h z. \<lbrakk>h \<in> Y; z \<in> K\<rbrakk> \<Longrightarrow> norm(h z) \<le> B"
-proof%unimportant -
+proof -
define U where "U \<equiv> {z \<in> S. \<exists>B Z. 0 < B \<and> open Z \<and> z \<in> Z \<and> Z \<subseteq> S \<and>
(\<forall>h z'. h \<in> Y \<and> z' \<in> Z \<longrightarrow> norm(h z') \<le> B)}"
then have "U \<subseteq> S" by blast
@@ -1432,11 +1432,11 @@
qed
-lemma%important GPicard4:
+lemma GPicard4:
assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})"
and AE: "\<And>e. \<lbrakk>0 < e; e < k\<rbrakk> \<Longrightarrow> \<exists>d. 0 < d \<and> d < e \<and> (\<forall>z \<in> sphere 0 d. norm(f z) \<le> B)"
obtains \<epsilon> where "0 < \<epsilon>" "\<epsilon> < k" "\<And>z. z \<in> ball 0 \<epsilon> - {0} \<Longrightarrow> norm(f z) \<le> B"
-proof%unimportant -
+proof -
obtain \<epsilon> where "0 < \<epsilon>" "\<epsilon> < k/2" and \<epsilon>: "\<And>z. norm z = \<epsilon> \<Longrightarrow> norm(f z) \<le> B"
using AE [of "k/2"] \<open>0 < k\<close> by auto
show ?thesis
@@ -1471,13 +1471,13 @@
qed
-lemma%important GPicard5:
+lemma GPicard5:
assumes holf: "f holomorphic_on (ball 0 1 - {0})"
and f01: "\<And>z. z \<in> ball 0 1 - {0} \<Longrightarrow> f z \<noteq> 0 \<and> f z \<noteq> 1"
obtains e B where "0 < e" "e < 1" "0 < B"
"(\<forall>z \<in> ball 0 e - {0}. norm(f z) \<le> B) \<or>
(\<forall>z \<in> ball 0 e - {0}. norm(f z) \<ge> B)"
-proof%unimportant -
+proof -
have [simp]: "1 + of_nat n \<noteq> (0::complex)" for n
using of_nat_eq_0_iff by fastforce
have [simp]: "cmod (1 + of_nat n) = 1 + of_nat n" for n
@@ -1614,13 +1614,13 @@
qed
-lemma%important GPicard6:
+lemma GPicard6:
assumes "open M" "z \<in> M" "a \<noteq> 0" and holf: "f holomorphic_on (M - {z})"
and f0a: "\<And>w. w \<in> M - {z} \<Longrightarrow> f w \<noteq> 0 \<and> f w \<noteq> a"
obtains r where "0 < r" "ball z r \<subseteq> M"
"bounded(f ` (ball z r - {z})) \<or>
bounded((inverse \<circ> f) ` (ball z r - {z}))"
-proof%unimportant -
+proof -
obtain r where "0 < r" and r: "ball z r \<subseteq> M"
using assms openE by blast
let ?g = "\<lambda>w. f (z + of_real r * w) / a"
@@ -1669,11 +1669,11 @@
qed
-theorem%important great_Picard:
+theorem great_Picard:
assumes "open M" "z \<in> M" "a \<noteq> b" and holf: "f holomorphic_on (M - {z})"
and fab: "\<And>w. w \<in> M - {z} \<Longrightarrow> f w \<noteq> a \<and> f w \<noteq> b"
obtains l where "(f \<longlongrightarrow> l) (at z) \<or> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
-proof%unimportant -
+proof -
obtain r where "0 < r" and zrM: "ball z r \<subseteq> M"
and r: "bounded((\<lambda>z. f z - a) ` (ball z r - {z})) \<or>
bounded((inverse \<circ> (\<lambda>z. f z - a)) ` (ball z r - {z}))"
@@ -1776,7 +1776,7 @@
qed
-corollary%important great_Picard_alt:
+corollary great_Picard_alt:
assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})"
and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
obtains a where "- {a} \<subseteq> f ` (M - {z})"
@@ -1784,11 +1784,11 @@
by%unimportant (metis great_Picard [OF M _ holf] non)
-corollary%important great_Picard_infinite:
+corollary great_Picard_infinite:
assumes M: "open M" "z \<in> M" and holf: "f holomorphic_on (M - {z})"
and non: "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
obtains a where "\<And>w. w \<noteq> a \<Longrightarrow> infinite {x. x \<in> M - {z} \<and> f x = w}"
-proof%unimportant -
+proof -
have False if "a \<noteq> b" and ab: "finite {x. x \<in> M - {z} \<and> f x = a}" "finite {x. x \<in> M - {z} \<and> f x = b}" for a b
proof -
have finab: "finite {x. x \<in> M - {z} \<and> f x \<in> {a,b}}"
@@ -1830,11 +1830,11 @@
by meson
qed
-corollary%important Casorati_Weierstrass:
+theorem Casorati_Weierstrass:
assumes "open M" "z \<in> M" "f holomorphic_on (M - {z})"
and "\<And>l. \<not> (f \<longlongrightarrow> l) (at z)" "\<And>l. \<not> ((inverse \<circ> f) \<longlongrightarrow> l) (at z)"
shows "closure(f ` (M - {z})) = UNIV"
-proof%unimportant -
+proof -
obtain a where a: "- {a} \<subseteq> f ` (M - {z})"
using great_Picard_alt [OF assms] .
have "UNIV = closure(- {a})"
--- a/src/HOL/Analysis/Homeomorphism.thy Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Homeomorphism.thy Thu Jan 17 15:50:28 2019 +0000
@@ -8,7 +8,7 @@
imports Homotopy
begin
-lemma%unimportant homeomorphic_spheres':
+lemma homeomorphic_spheres':
fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space"
assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)"
shows "(sphere a \<delta>) homeomorphic (sphere b \<delta>)"
@@ -28,7 +28,7 @@
done
qed
-lemma%unimportant homeomorphic_spheres_gen:
+lemma homeomorphic_spheres_gen:
fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space"
assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)"
shows "(sphere a r homeomorphic sphere b s)"
@@ -38,7 +38,7 @@
subsection%important \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
-proposition%important ray_to_rel_frontier:
+proposition ray_to_rel_frontier:
fixes a :: "'a::real_inner"
assumes "bounded S"
and a: "a \<in> rel_interior S"
@@ -46,7 +46,7 @@
and "l \<noteq> 0"
obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S"
"\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
-proof%unimportant -
+proof -
have aaff: "a \<in> affine hull S"
by (meson a hull_subset rel_interior_subset rev_subsetD)
let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
@@ -139,14 +139,14 @@
by (rule that [OF \<open>0 < d\<close> infront inint])
qed
-corollary%important ray_to_frontier:
+corollary ray_to_frontier:
fixes a :: "'a::euclidean_space"
assumes "bounded S"
and a: "a \<in> interior S"
and "l \<noteq> 0"
obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S"
"\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S"
-proof%unimportant -
+proof -
have "interior S = rel_interior S"
using a rel_interior_nonempty_interior by auto
then have "a \<in> rel_interior S"
@@ -158,7 +158,7 @@
qed
-lemma%unimportant segment_to_rel_frontier_aux:
+lemma segment_to_rel_frontier_aux:
fixes x :: "'a::euclidean_space"
assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y"
obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
@@ -198,7 +198,7 @@
qed
qed
-lemma%unimportant segment_to_rel_frontier:
+lemma segment_to_rel_frontier:
fixes x :: "'a::euclidean_space"
assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
@@ -216,11 +216,11 @@
using segment_to_rel_frontier_aux [OF S x y] that by blast
qed
-proposition%important rel_frontier_not_sing:
+proposition rel_frontier_not_sing:
fixes a :: "'a::euclidean_space"
assumes "bounded S"
shows "rel_frontier S \<noteq> {a}"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True then show ?thesis by simp
next
case False
@@ -278,7 +278,7 @@
qed
qed
-proposition%important
+proposition (*FIXME needs name *)
fixes S :: "'a::euclidean_space set"
assumes "compact S" and 0: "0 \<in> rel_interior S"
and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment 0 x \<subseteq> rel_interior S"
@@ -288,7 +288,7 @@
and starlike_compact_projective2_0:
"S homeomorphic cball 0 1 \<inter> affine hull S"
(is "S homeomorphic ?CBALL")
-proof%unimportant -
+proof -
have starI: "(u *\<^sub>R x) \<in> rel_interior S" if "x \<in> S" "0 \<le> u" "u < 1" for x u
proof (cases "x=0 \<or> u=0")
case True with 0 show ?thesis by force
@@ -540,7 +540,7 @@
done
qed
-corollary%important
+corollary (* FIXME needs name *)
fixes S :: "'a::euclidean_space set"
assumes "compact S" and a: "a \<in> rel_interior S"
and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
@@ -548,7 +548,7 @@
"S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S"
and starlike_compact_projective2:
"S homeomorphic cball a 1 \<inter> affine hull S"
-proof%unimportant -
+proof -
have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation)
have 2: "0 \<in> rel_interior ((+) (-a) ` S)"
using a rel_interior_translation [of "- a" S] by (simp cong: image_cong_simp)
@@ -580,12 +580,12 @@
finally show "S homeomorphic cball a 1 \<inter> affine hull S" .
qed
-corollary%important starlike_compact_projective_special:
+corollary starlike_compact_projective_special:
assumes "compact S"
and cb01: "cball (0::'a::euclidean_space) 1 \<subseteq> S"
and scale: "\<And>x u. \<lbrakk>x \<in> S; 0 \<le> u; u < 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x \<in> S - frontier S"
shows "S homeomorphic (cball (0::'a::euclidean_space) 1)"
-proof%unimportant -
+proof -
have "ball 0 1 \<subseteq> interior S"
using cb01 interior_cball interior_mono by blast
then have 0: "0 \<in> rel_interior S"
@@ -604,13 +604,13 @@
using starlike_compact_projective2_0 [OF \<open>compact S\<close> 0 star] by simp
qed
-lemma%important homeomorphic_convex_lemma:
+lemma homeomorphic_convex_lemma:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "convex S" "compact S" "convex T" "compact T"
and affeq: "aff_dim S = aff_dim T"
shows "(S - rel_interior S) homeomorphic (T - rel_interior T) \<and>
S homeomorphic T"
-proof%unimportant (cases "rel_interior S = {} \<or> rel_interior T = {}")
+proof (cases "rel_interior S = {} \<or> rel_interior T = {}")
case True
then show ?thesis
by (metis Diff_empty affeq \<open>convex S\<close> \<open>convex T\<close> aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty)
@@ -708,7 +708,7 @@
using 1 2 by blast
qed
-lemma%unimportant homeomorphic_convex_compact_sets:
+lemma homeomorphic_convex_compact_sets:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "convex S" "compact S" "convex T" "compact T"
and affeq: "aff_dim S = aff_dim T"
@@ -716,7 +716,7 @@
using homeomorphic_convex_lemma [OF assms] assms
by (auto simp: rel_frontier_def)
-lemma%unimportant homeomorphic_rel_frontiers_convex_bounded_sets:
+lemma homeomorphic_rel_frontiers_convex_bounded_sets:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "convex S" "bounded S" "convex T" "bounded T"
and affeq: "aff_dim S = aff_dim T"
@@ -729,7 +729,7 @@
text\<open>Including the famous stereoscopic projection of the 3-D sphere to the complex plane\<close>
text\<open>The special case with centre 0 and radius 1\<close>
-lemma%unimportant homeomorphic_punctured_affine_sphere_affine_01:
+lemma homeomorphic_punctured_affine_sphere_affine_01:
assumes "b \<in> sphere 0 1" "affine T" "0 \<in> T" "b \<in> T" "affine p"
and affT: "aff_dim T = aff_dim p + 1"
shows "(sphere 0 1 \<inter> T) - {b} homeomorphic p"
@@ -823,12 +823,12 @@
finally show ?thesis .
qed
-theorem%important homeomorphic_punctured_affine_sphere_affine:
+theorem homeomorphic_punctured_affine_sphere_affine:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p"
and aff: "aff_dim T = aff_dim p + 1"
shows "(sphere a r \<inter> T) - {b} homeomorphic p"
-proof%unimportant -
+proof -
have "a \<noteq> b" using assms by auto
then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))"
by (simp add: inj_on_def)
@@ -847,14 +847,14 @@
finally show ?thesis .
qed
-corollary%important homeomorphic_punctured_sphere_affine:
+corollary homeomorphic_punctured_sphere_affine:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" and b: "b \<in> sphere a r"
and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
shows "(sphere a r - {b}) homeomorphic T"
using%unimportant homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by%unimportant auto
-corollary%important homeomorphic_punctured_sphere_hyperplane:
+corollary homeomorphic_punctured_sphere_hyperplane:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" and b: "b \<in> sphere a r"
and "c \<noteq> 0"
@@ -864,12 +864,12 @@
apply (auto simp: affine_hyperplane of_nat_diff)
done
-proposition%important homeomorphic_punctured_sphere_affine_gen:
+proposition homeomorphic_punctured_sphere_affine_gen:
fixes a :: "'a :: euclidean_space"
assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S"
and "affine T" and affS: "aff_dim S = aff_dim T + 1"
shows "rel_frontier S - {a} homeomorphic T"
-proof%unimportant -
+proof -
obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S"
using choose_affine_subset [OF affine_UNIV aff_dim_geq]
by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex)
@@ -912,13 +912,13 @@
is homeomorphic to a closed subset of a convex set, and
if the set is locally compact we can take the convex set to be the universe.\<close>
-proposition%important homeomorphic_closedin_convex:
+proposition homeomorphic_closedin_convex:
fixes S :: "'m::euclidean_space set"
assumes "aff_dim S < DIM('n)"
obtains U and T :: "'n::euclidean_space set"
where "convex U" "U \<noteq> {}" "closedin (subtopology euclidean U) T"
"S homeomorphic T"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True then show ?thesis
by (rule_tac U=UNIV and T="{}" in that) auto
next
@@ -1009,11 +1009,11 @@
text\<open> Locally compact sets are closed in an open set and are homeomorphic
to an absolutely closed set if we have one more dimension to play with.\<close>
-lemma%important locally_compact_open_Int_closure:
+lemma locally_compact_open_Int_closure:
fixes S :: "'a :: metric_space set"
assumes "locally compact S"
obtains T where "open T" "S = T \<inter> closure S"
-proof%unimportant -
+proof -
have "\<forall>x\<in>S. \<exists>T v u. u = S \<inter> T \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<and> open T \<and> compact v"
by (metis assms locally_compact openin_open)
then obtain t v where
@@ -1048,14 +1048,14 @@
qed
-lemma%unimportant locally_compact_closedin_open:
+lemma locally_compact_closedin_open:
fixes S :: "'a :: metric_space set"
assumes "locally compact S"
obtains T where "open T" "closedin (subtopology euclidean T) S"
by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int)
-lemma%unimportant locally_compact_homeomorphism_projection_closed:
+lemma locally_compact_homeomorphism_projection_closed:
assumes "locally compact S"
obtains T and f :: "'a \<Rightarrow> 'a :: euclidean_space \<times> 'b :: euclidean_space"
where "closed T" "homeomorphism S T f fst"
@@ -1108,14 +1108,14 @@
done
qed
-lemma%unimportant locally_compact_closed_Int_open:
+lemma locally_compact_closed_Int_open:
fixes S :: "'a :: euclidean_space set"
shows
"locally compact S \<longleftrightarrow> (\<exists>U u. closed U \<and> open u \<and> S = U \<inter> u)"
by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact)
-lemma%unimportant lowerdim_embeddings:
+lemma lowerdim_embeddings:
assumes "DIM('a) < DIM('b)"
obtains f :: "'a::euclidean_space*real \<Rightarrow> 'b::euclidean_space"
and g :: "'b \<Rightarrow> 'a*real"
@@ -1161,11 +1161,11 @@
qed
qed
-proposition%important locally_compact_homeomorphic_closed:
+proposition locally_compact_homeomorphic_closed:
fixes S :: "'a::euclidean_space set"
assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)"
obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T"
-proof%unimportant -
+proof -
obtain U:: "('a*real)set" and h
where "closed U" and homU: "homeomorphism S U h fst"
using locally_compact_homeomorphism_projection_closed assms by metis
@@ -1191,13 +1191,13 @@
qed
-lemma%important homeomorphic_convex_compact_lemma:
+lemma homeomorphic_convex_compact_lemma:
fixes S :: "'a::euclidean_space set"
assumes "convex S"
and "compact S"
and "cball 0 1 \<subseteq> S"
shows "S homeomorphic (cball (0::'a) 1)"
-proof%unimportant (rule starlike_compact_projective_special[OF assms(2-3)])
+proof (rule starlike_compact_projective_special[OF assms(2-3)])
fix x u
assume "x \<in> S" and "0 \<le> u" and "u < (1::real)"
have "open (ball (u *\<^sub>R x) (1 - u))"
@@ -1223,7 +1223,7 @@
using frontier_def and interior_subset by auto
qed
-proposition%important homeomorphic_convex_compact_cball:
+proposition homeomorphic_convex_compact_cball:
fixes e :: real
and S :: "'a::euclidean_space set"
assumes "convex S"
@@ -1231,7 +1231,7 @@
and "interior S \<noteq> {}"
and "e > 0"
shows "S homeomorphic (cball (b::'a) e)"
-proof%unimportant -
+proof -
obtain a where "a \<in> interior S"
using assms(3) by auto
then obtain d where "d > 0" and d: "cball a d \<subseteq> S"
@@ -1259,7 +1259,7 @@
done
qed
-corollary%important homeomorphic_convex_compact:
+corollary homeomorphic_convex_compact:
fixes S :: "'a::euclidean_space set"
and T :: "'a set"
assumes "convex S" "compact S" "interior S \<noteq> {}"
@@ -1268,7 +1268,7 @@
using assms
by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
-subsection%important\<open>Covering spaces and lifting results for them\<close>
+subsection\<open>Covering spaces and lifting results for them\<close>
definition%important covering_space
:: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
@@ -1281,19 +1281,19 @@
pairwise disjnt v \<and>
(\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
-lemma%unimportant covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
+lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
by (simp add: covering_space_def)
-lemma%unimportant covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
+lemma covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
by (simp add: covering_space_def)
-lemma%unimportant homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
+lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
apply (simp add: homeomorphism_def covering_space_def, clarify)
apply (rule_tac x=T in exI, simp)
apply (rule_tac x="{S}" in exI, auto)
done
-lemma%unimportant covering_space_local_homeomorphism:
+lemma covering_space_local_homeomorphism:
assumes "covering_space c p S" "x \<in> c"
obtains T u q where "x \<in> T" "openin (subtopology euclidean c) T"
"p x \<in> u" "openin (subtopology euclidean S) u"
@@ -1304,13 +1304,13 @@
by (metis IntI UnionE vimage_eq)
-lemma%important covering_space_local_homeomorphism_alt:
+lemma covering_space_local_homeomorphism_alt:
assumes p: "covering_space c p S" and "y \<in> S"
obtains x T U q where "p x = y"
"x \<in> T" "openin (subtopology euclidean c) T"
"y \<in> U" "openin (subtopology euclidean S) U"
"homeomorphism T U p q"
-proof%unimportant -
+proof -
obtain x where "p x = y" "x \<in> c"
using assms covering_space_imp_surjective by blast
show ?thesis
@@ -1318,11 +1318,11 @@
using that \<open>p x = y\<close> by blast
qed
-proposition%important covering_space_open_map:
+proposition covering_space_open_map:
fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set"
assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T"
shows "openin (subtopology euclidean S) (p ` T)"
-proof%unimportant -
+proof -
have pce: "p ` c = S"
and covs:
"\<And>x. x \<in> S \<Longrightarrow>
@@ -1368,7 +1368,7 @@
with openin_subopen show ?thesis by blast
qed
-lemma%important covering_space_lift_unique_gen:
+lemma covering_space_lift_unique_gen:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
assumes cov: "covering_space c p S"
@@ -1380,7 +1380,7 @@
and fg2: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
and u_compt: "U \<in> components T" and "a \<in> U" "x \<in> U"
shows "g1 x = g2 x"
-proof%unimportant -
+proof -
have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
define G12 where "G12 \<equiv> {x \<in> U. g1 x - g2 x = 0}"
have "connected U" by (rule in_components_connected [OF u_compt])
@@ -1427,7 +1427,7 @@
using \<open>x \<in> U\<close> by force
qed
-proposition%important covering_space_lift_unique:
+proposition covering_space_lift_unique:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
assumes "covering_space c p S"
@@ -1437,10 +1437,10 @@
"continuous_on T g2" "g2 ` T \<subseteq> c" "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
"connected T" "a \<in> T" "x \<in> T"
shows "g1 x = g2 x"
- using%unimportant covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
- by%unimportant blast
+ using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
+ by blast
-lemma%unimportant covering_space_locally:
+lemma covering_space_locally:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes loc: "locally \<phi> C" and cov: "covering_space C p S"
and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
@@ -1456,14 +1456,14 @@
qed
-proposition%important covering_space_locally_eq:
+proposition covering_space_locally_eq:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
and qim: "\<And>q U. \<lbrakk>U \<subseteq> S; continuous_on U q; \<psi> U\<rbrakk> \<Longrightarrow> \<phi>(q ` U)"
shows "locally \<psi> S \<longleftrightarrow> locally \<phi> C"
(is "?lhs = ?rhs")
-proof%unimportant
+proof
assume L: ?lhs
show ?rhs
proof (rule locallyI)
@@ -1518,7 +1518,7 @@
using cov covering_space_locally pim by blast
qed
-lemma%unimportant covering_space_locally_compact_eq:
+lemma covering_space_locally_compact_eq:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "covering_space C p S"
shows "locally compact S \<longleftrightarrow> locally compact C"
@@ -1526,7 +1526,7 @@
apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
using compact_continuous_image by blast
-lemma%unimportant covering_space_locally_connected_eq:
+lemma covering_space_locally_connected_eq:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "covering_space C p S"
shows "locally connected S \<longleftrightarrow> locally connected C"
@@ -1534,7 +1534,7 @@
apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
using connected_continuous_image by blast
-lemma%unimportant covering_space_locally_path_connected_eq:
+lemma covering_space_locally_path_connected_eq:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "covering_space C p S"
shows "locally path_connected S \<longleftrightarrow> locally path_connected C"
@@ -1543,26 +1543,26 @@
using path_connected_continuous_image by blast
-lemma%unimportant covering_space_locally_compact:
+lemma covering_space_locally_compact:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "locally compact C" "covering_space C p S"
shows "locally compact S"
using assms covering_space_locally_compact_eq by blast
-lemma%unimportant covering_space_locally_connected:
+lemma covering_space_locally_connected:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "locally connected C" "covering_space C p S"
shows "locally connected S"
using assms covering_space_locally_connected_eq by blast
-lemma%unimportant covering_space_locally_path_connected:
+lemma covering_space_locally_path_connected:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "locally path_connected C" "covering_space C p S"
shows "locally path_connected S"
using assms covering_space_locally_path_connected_eq by blast
-proposition%important covering_space_lift_homotopy:
+proposition covering_space_lift_homotopy:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and h :: "real \<times> 'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S"
@@ -1574,7 +1574,7 @@
"k ` ({0..1} \<times> U) \<subseteq> C"
"\<And>y. y \<in> U \<Longrightarrow> k(0, y) = f y"
"\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p(k z)"
-proof%unimportant -
+proof -
have "\<exists>V k. openin (subtopology euclidean U) V \<and> y \<in> V \<and>
continuous_on ({0..1} \<times> V) k \<and> k ` ({0..1} \<times> V) \<subseteq> C \<and>
(\<forall>z \<in> V. k(0, z) = f z) \<and> (\<forall>z \<in> {0..1} \<times> V. h z = p(k z))"
@@ -1912,7 +1912,7 @@
qed (auto simp: contk)
qed
-corollary%important covering_space_lift_homotopy_alt:
+corollary covering_space_lift_homotopy_alt:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and h :: "'c::real_normed_vector \<times> real \<Rightarrow> 'b"
assumes cov: "covering_space C p S"
@@ -1924,7 +1924,7 @@
"k ` (U \<times> {0..1}) \<subseteq> C"
"\<And>y. y \<in> U \<Longrightarrow> k(y, 0) = f y"
"\<And>z. z \<in> U \<times> {0..1} \<Longrightarrow> h z = p(k z)"
-proof%unimportant -
+proof -
have "continuous_on ({0..1} \<times> U) (h \<circ> (\<lambda>z. (snd z, fst z)))"
by (intro continuous_intros continuous_on_subset [OF conth]) auto
then obtain k where contk: "continuous_on ({0..1} \<times> U) k"
@@ -1940,7 +1940,7 @@
done
qed
-corollary%important covering_space_lift_homotopic_function:
+corollary covering_space_lift_homotopic_function:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and g:: "'c::real_normed_vector \<Rightarrow> 'a"
assumes cov: "covering_space C p S"
and contg: "continuous_on U g"
@@ -1948,7 +1948,7 @@
and pgeq: "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
and hom: "homotopic_with (\<lambda>x. True) U S f f'"
obtains g' where "continuous_on U g'" "image g' U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g' y) = f' y"
-proof%unimportant -
+proof -
obtain h where conth: "continuous_on ({0..1::real} \<times> U) h"
and him: "h ` ({0..1} \<times> U) \<subseteq> S"
and h0: "\<And>x. h(0, x) = f x"
@@ -1972,12 +1972,12 @@
qed
qed
-corollary%important covering_space_lift_inessential_function:
+corollary covering_space_lift_inessential_function:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and U :: "'c::real_normed_vector set"
assumes cov: "covering_space C p S"
and hom: "homotopic_with (\<lambda>x. True) U S f (\<lambda>x. a)"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (cases "U = {}")
+proof (cases "U = {}")
case True
then show ?thesis
using that continuous_on_empty by blast
@@ -1997,14 +1997,14 @@
subsection%important\<open> Lifting of general functions to covering space\<close>
-proposition%important covering_space_lift_path_strong:
+proposition covering_space_lift_path_strong:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" and "a \<in> C"
and "path g" and pag: "path_image g \<subseteq> S" and pas: "pathstart g = p a"
obtains h where "path h" "path_image h \<subseteq> C" "pathstart h = a"
and "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = g t"
-proof%unimportant -
+proof -
obtain k:: "real \<times> 'c \<Rightarrow> 'a"
where contk: "continuous_on ({0..1} \<times> {undefined}) k"
and kim: "k ` ({0..1} \<times> {undefined}) \<subseteq> C"
@@ -2033,11 +2033,11 @@
qed
qed
-corollary%important covering_space_lift_path:
+corollary covering_space_lift_path:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes cov: "covering_space C p S" and "path g" and pig: "path_image g \<subseteq> S"
obtains h where "path h" "path_image h \<subseteq> C" "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = g t"
-proof%unimportant -
+proof -
obtain a where "a \<in> C" "pathstart g = p a"
by (metis pig cov covering_space_imp_surjective imageE pathstart_in_path_image subsetCE)
show ?thesis
@@ -2046,7 +2046,7 @@
qed
-proposition%important covering_space_lift_homotopic_paths:
+proposition covering_space_lift_homotopic_paths:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and "path g1" and pig1: "path_image g1 \<subseteq> S"
@@ -2056,7 +2056,7 @@
and "path h2" and pih2: "path_image h2 \<subseteq> C" and ph2: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h2 t) = g2 t"
and h1h2: "pathstart h1 = pathstart h2"
shows "homotopic_paths C h1 h2"
-proof%unimportant -
+proof -
obtain h :: "real \<times> real \<Rightarrow> 'b"
where conth: "continuous_on ({0..1} \<times> {0..1}) h"
and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
@@ -2117,7 +2117,7 @@
qed
-corollary%important covering_space_monodromy:
+corollary covering_space_monodromy:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and "path g1" and pig1: "path_image g1 \<subseteq> S"
@@ -2131,7 +2131,7 @@
by%unimportant blast
-corollary%important covering_space_lift_homotopic_path:
+corollary covering_space_lift_homotopic_path:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and hom: "homotopic_paths S f f'"
@@ -2140,7 +2140,7 @@
and pgeq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(g t) = f t"
obtains g' where "path g'" "path_image g' \<subseteq> C"
"pathstart g' = a" "pathfinish g' = b" "\<And>t. t \<in> {0..1} \<Longrightarrow> p(g' t) = f' t"
-proof%unimportant (rule covering_space_lift_path_strong [OF cov, of a f'])
+proof (rule covering_space_lift_path_strong [OF cov, of a f'])
show "a \<in> C"
using a pig by auto
show "path f'" "path_image f' \<subseteq> S"
@@ -2150,7 +2150,7 @@
qed (metis (mono_tags, lifting) assms cov covering_space_monodromy hom homotopic_paths_imp_path homotopic_paths_imp_subset pgeq pig)
-proposition%important covering_space_lift_general:
+proposition covering_space_lift_general:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" and "a \<in> C" "z \<in> U"
@@ -2162,7 +2162,7 @@
pathstart q = a \<and> pathfinish q = a \<and>
homotopic_paths S (f \<circ> r) (p \<circ> q)"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant -
+proof -
have *: "\<exists>g h. path g \<and> path_image g \<subseteq> U \<and>
pathstart g = z \<and> pathfinish g = y \<and>
path h \<and> path_image h \<subseteq> C \<and> pathstart h = a \<and>
@@ -2405,7 +2405,7 @@
qed
-corollary%important covering_space_lift_stronger:
+corollary covering_space_lift_stronger:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
@@ -2415,7 +2415,7 @@
and hom: "\<And>r. \<lbrakk>path r; path_image r \<subseteq> U; pathstart r = z; pathfinish r = z\<rbrakk>
\<Longrightarrow> \<exists>b. homotopic_paths S (f \<circ> r) (linepath b b)"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (rule covering_space_lift_general [OF cov U contf fim feq])
+proof (rule covering_space_lift_general [OF cov U contf fim feq])
fix r
assume "path r" "path_image r \<subseteq> U" "pathstart r = z" "pathfinish r = z"
then obtain b where b: "homotopic_paths S (f \<circ> r) (linepath b b)"
@@ -2432,7 +2432,7 @@
by (force simp: \<open>a \<in> C\<close>)
qed auto
-corollary%important covering_space_lift_strong:
+corollary covering_space_lift_strong:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
@@ -2440,7 +2440,7 @@
and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
and feq: "f z = p a"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
+proof (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
show "path_connected U"
using scU simply_connected_eq_contractible_loop_some by blast
fix r
@@ -2453,14 +2453,14 @@
by blast
qed blast
-corollary%important covering_space_lift:
+corollary covering_space_lift:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S"
and U: "simply_connected U" "locally path_connected U"
and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (cases "U = {}")
+proof (cases "U = {}")
case True
with that show ?thesis by auto
next
--- a/src/HOL/Analysis/Improper_Integral.thy Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Improper_Integral.thy Thu Jan 17 15:50:28 2019 +0000
@@ -28,11 +28,11 @@
unfolding equiintegrable_on_def Ball_def
by (erule conj_forward imp_forward all_forward ex_forward | blast)+
-lemma%important equiintegrable_on_Un:
+lemma equiintegrable_on_Un:
assumes "F equiintegrable_on I" "G equiintegrable_on I"
shows "(F \<union> G) equiintegrable_on I"
unfolding equiintegrable_on_def
-proof%unimportant (intro conjI impI allI)
+proof (intro conjI impI allI)
show "\<forall>f\<in>F \<union> G. f integrable_on I"
using assms unfolding equiintegrable_on_def by blast
show "\<exists>\<gamma>. gauge \<gamma> \<and>
@@ -76,12 +76,12 @@
text\<open> Main limit theorem for an equiintegrable sequence.\<close>
-theorem%important equiintegrable_limit:
+theorem equiintegrable_limit:
fixes g :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
assumes feq: "range f equiintegrable_on cbox a b"
and to_g: "\<And>x. x \<in> cbox a b \<Longrightarrow> (\<lambda>n. f n x) \<longlonglongrightarrow> g x"
shows "g integrable_on cbox a b \<and> (\<lambda>n. integral (cbox a b) (f n)) \<longlonglongrightarrow> integral (cbox a b) g"
-proof%unimportant -
+proof -
have "Cauchy (\<lambda>n. integral(cbox a b) (f n))"
proof (clarsimp simp add: Cauchy_def)
fix e::real
@@ -151,10 +151,10 @@
qed
-lemma%important equiintegrable_reflect:
+lemma equiintegrable_reflect:
assumes "F equiintegrable_on cbox a b"
shows "(\<lambda>f. f \<circ> uminus) ` F equiintegrable_on cbox (-b) (-a)"
-proof%unimportant -
+proof -
have "\<exists>\<gamma>. gauge \<gamma> \<and>
(\<forall>f \<D>. f \<in> (\<lambda>f. f \<circ> uminus) ` F \<and> \<D> tagged_division_of cbox (- b) (- a) \<and> \<gamma> fine \<D> \<longrightarrow>
norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - integral (cbox (- b) (- a)) f) < e)"
@@ -246,13 +246,13 @@
qed
-lemma%important content_division_lemma1:
+lemma content_division_lemma1:
assumes div: "\<D> division_of S" and S: "S \<subseteq> cbox a b" and i: "i \<in> Basis"
and mt: "\<And>K. K \<in> \<D> \<Longrightarrow> content K \<noteq> 0"
and disj: "(\<forall>K \<in> \<D>. K \<inter> {x. x \<bullet> i = a \<bullet> i} \<noteq> {}) \<or> (\<forall>K \<in> \<D>. K \<inter> {x. x \<bullet> i = b \<bullet> i} \<noteq> {})"
shows "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
\<le> content(cbox a b)" (is "?lhs \<le> ?rhs")
-proof%unimportant -
+proof -
have "finite \<D>"
using div by blast
define extend where
@@ -409,13 +409,13 @@
qed
-proposition%important sum_content_area_over_thin_division:
+proposition sum_content_area_over_thin_division:
assumes div: "\<D> division_of S" and S: "S \<subseteq> cbox a b" and i: "i \<in> Basis"
and "a \<bullet> i \<le> c" "c \<le> b \<bullet> i"
and nonmt: "\<And>K. K \<in> \<D> \<Longrightarrow> K \<inter> {x. x \<bullet> i = c} \<noteq> {}"
shows "(b \<bullet> i - a \<bullet> i) * (\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))
\<le> 2 * content(cbox a b)"
-proof%unimportant (cases "content(cbox a b) = 0")
+proof (cases "content(cbox a b) = 0")
case True
have "(\<Sum>K\<in>\<D>. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)) = 0"
using S div by (force intro!: sum.neutral content_0_subset [OF True])
@@ -609,7 +609,7 @@
-proposition%important bounded_equiintegral_over_thin_tagged_partial_division:
+proposition bounded_equiintegral_over_thin_tagged_partial_division:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F" and "0 < \<epsilon>"
and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
@@ -617,7 +617,7 @@
"\<And>c i S h. \<lbrakk>c \<in> cbox a b; i \<in> Basis; S tagged_partial_division_of cbox a b;
\<gamma> fine S; h \<in> F; \<And>x K. (x,K) \<in> S \<Longrightarrow> (K \<inter> {x. x \<bullet> i = c \<bullet> i} \<noteq> {})\<rbrakk>
\<Longrightarrow> (\<Sum>(x,K) \<in> S. norm (integral K h)) < \<epsilon>"
-proof%unimportant (cases "content(cbox a b) = 0")
+proof (cases "content(cbox a b) = 0")
case True
show ?thesis
proof
@@ -813,13 +813,13 @@
-proposition%important equiintegrable_halfspace_restrictions_le:
+proposition equiintegrable_halfspace_restrictions_le:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i \<le> c then h x else 0)})
equiintegrable_on cbox a b"
-proof%unimportant (cases "content(cbox a b) = 0")
+proof (cases "content(cbox a b) = 0")
case True
then show ?thesis by simp
next
@@ -1172,13 +1172,13 @@
-corollary%important equiintegrable_halfspace_restrictions_ge:
+corollary equiintegrable_halfspace_restrictions_ge:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes F: "F equiintegrable_on cbox a b" and f: "f \<in> F"
and norm_f: "\<And>h x. \<lbrakk>h \<in> F; x \<in> cbox a b\<rbrakk> \<Longrightarrow> norm(h x) \<le> norm(f x)"
shows "(\<Union>i \<in> Basis. \<Union>c. \<Union>h \<in> F. {(\<lambda>x. if x \<bullet> i \<ge> c then h x else 0)})
equiintegrable_on cbox a b"
-proof%unimportant -
+proof -
have *: "(\<Union>i\<in>Basis. \<Union>c. \<Union>h\<in>(\<lambda>f. f \<circ> uminus) ` F. {\<lambda>x. if x \<bullet> i \<le> c then h x else 0})
equiintegrable_on cbox (- b) (- a)"
proof (rule equiintegrable_halfspace_restrictions_le)
@@ -1203,11 +1203,11 @@
qed
-proposition%important equiintegrable_closed_interval_restrictions:
+proposition equiintegrable_closed_interval_restrictions:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes f: "f integrable_on cbox a b"
shows "(\<Union>c d. {(\<lambda>x. if x \<in> cbox c d then f x else 0)}) equiintegrable_on cbox a b"
-proof%unimportant -
+proof -
let ?g = "\<lambda>B c d x. if \<forall>i\<in>B. c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i then f x else 0"
have *: "insert f (\<Union>c d. {?g B c d}) equiintegrable_on cbox a b" if "B \<subseteq> Basis" for B
proof -
@@ -1266,14 +1266,14 @@
subsection%important\<open>Continuity of the indefinite integral\<close>
-proposition%important indefinite_integral_continuous:
+proposition indefinite_integral_continuous:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes int_f: "f integrable_on cbox a b"
and c: "c \<in> cbox a b" and d: "d \<in> cbox a b" "0 < \<epsilon>"
obtains \<delta> where "0 < \<delta>"
"\<And>c' d'. \<lbrakk>c' \<in> cbox a b; d' \<in> cbox a b; norm(c' - c) \<le> \<delta>; norm(d' - d) \<le> \<delta>\<rbrakk>
\<Longrightarrow> norm(integral(cbox c' d') f - integral(cbox c d) f) < \<epsilon>"
-proof%unimportant -
+proof -
{ assume "\<exists>c' d'. c' \<in> cbox a b \<and> d' \<in> cbox a b \<and> norm(c' - c) \<le> \<delta> \<and> norm(d' - d) \<le> \<delta> \<and>
norm(integral(cbox c' d') f - integral(cbox c d) f) \<ge> \<epsilon>"
(is "\<exists>c' d'. ?\<Phi> c' d' \<delta>") if "0 < \<delta>" for \<delta>
@@ -1358,11 +1358,11 @@
by (meson not_le that)
qed
-corollary%important indefinite_integral_uniformly_continuous:
+corollary indefinite_integral_uniformly_continuous:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes "f integrable_on cbox a b"
shows "uniformly_continuous_on (cbox (Pair a a) (Pair b b)) (\<lambda>y. integral (cbox (fst y) (snd y)) f)"
-proof%unimportant -
+proof -
show ?thesis
proof (rule compact_uniformly_continuous, clarsimp simp add: continuous_on_iff)
fix c d and \<epsilon>::real
@@ -1383,11 +1383,11 @@
qed
-corollary%important bounded_integrals_over_subintervals:
+corollary bounded_integrals_over_subintervals:
fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
assumes "f integrable_on cbox a b"
shows "bounded {integral (cbox c d) f |c d. cbox c d \<subseteq> cbox a b}"
-proof%unimportant -
+proof -
have "bounded ((\<lambda>y. integral (cbox (fst y) (snd y)) f) ` cbox (a, a) (b, b))"
(is "bounded ?I")
by (blast intro: bounded_cbox bounded_uniformly_continuous_image indefinite_integral_uniformly_continuous [OF assms])
@@ -1414,7 +1414,7 @@
We only need to assume that the integrals are bounded, and we get absolute integrability,
but we also need a (rather weak) bound assumption on the function.\<close>
-theorem%important absolutely_integrable_improper:
+theorem absolutely_integrable_improper:
fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
assumes int_f: "\<And>c d. cbox c d \<subseteq> box a b \<Longrightarrow> f integrable_on cbox c d"
and bo: "bounded {integral (cbox c d) f |c d. cbox c d \<subseteq> box a b}"
@@ -1422,7 +1422,7 @@
\<Longrightarrow> \<exists>g. g absolutely_integrable_on cbox a b \<and>
((\<forall>x \<in> cbox a b. f x \<bullet> i \<le> g x) \<or> (\<forall>x \<in> cbox a b. f x \<bullet> i \<ge> g x))"
shows "f absolutely_integrable_on cbox a b"
-proof%unimportant (cases "content(cbox a b) = 0")
+proof (cases "content(cbox a b) = 0")
case True
then show ?thesis
by auto
--- a/src/HOL/Analysis/Interval_Integral.thy Wed Jan 16 21:27:33 2019 +0000
+++ b/src/HOL/Analysis/Interval_Integral.thy Thu Jan 17 15:50:28 2019 +0000
@@ -4,15 +4,15 @@
Lebesgue integral over an interval (with endpoints possibly +-\<infinity>)
*)
-theory Interval_Integral
+theory Interval_Integral (*FIX ME rename? Lebesgue *)
imports Equivalence_Lebesgue_Henstock_Integration
begin
-lemma%important continuous_on_vector_derivative:
+lemma continuous_on_vector_derivative:
"(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
- by%unimportant (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
+ by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
-definition%important "einterval a b = {x. a < ereal x \<and> ereal x < b}"
+definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
lemma einterval_eq[simp]:
shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}"
@@ -37,16 +37,16 @@
lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
unfolding einterval_def by measurable
-subsection\<open>Approximating a (possibly infinite) interval\<close>
+subsection%important \<open>Approximating a (possibly infinite) interval\<close>
lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
unfolding filterlim_def by (auto intro: le_supI1)
-lemma%important ereal_incseq_approx:
+lemma ereal_incseq_approx:
fixes a b :: ereal
assumes "a < b"
obtains X :: "nat \<Rightarrow> real" where "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
-proof%unimportant (cases b)
+proof (cases b)
case PInf
with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
by (cases a) auto
@@ -78,12 +78,12 @@
(auto simp: real incseq_def intro!: divide_left_mono)
qed (insert \<open>a < b\<close>, auto)
-lemma%important ereal_decseq_approx:
+lemma ereal_decseq_approx:
fixes a b :: ereal
assumes "a < b"
obtains X :: "nat \<Rightarrow> real" where
"decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a"
-proof%unimportant -
+proof -
have "-b < -a" using \<open>a < b\<close> by simp
from ereal_incseq_approx[OF this] guess X .
then show thesis
@@ -93,14 +93,14 @@
done
qed
-lemma%important einterval_Icc_approximation:
+proposition einterval_Icc_approximation:
fixes a b :: ereal
assumes "a < b"
obtains u l :: "nat \<Rightarrow> real" where
"einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
"l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
-proof%unimportant -
+proof -
from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe
from ereal_incseq_approx[OF \<open>c < b\<close>] guess u . note u = this
from ereal_decseq_approx[OF \<open>a < c\<close>] guess l . note l = this
@@ -202,17 +202,17 @@
interval_lebesgue_integrable M a b (\<lambda>x. c * f x)"
by (simp add: interval_lebesgue_integrable_def)
-lemma%important interval_lebesgue_integrable_mult_left [intro, simp]:
+lemma interval_lebesgue_integrable_mult_left [intro, simp]:
fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
interval_lebesgue_integrable M a b (\<lambda>x. f x * c)"
- by%unimportant (simp add: interval_lebesgue_integrable_def)
+ by (simp add: interval_lebesgue_integrable_def)
-lemma%important interval_lebesgue_integrable_divide [intro, simp]:
+lemma interval_lebesgue_integrable_divide [intro, simp]:
fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
interval_lebesgue_integrable M a b (\<lambda>x. f x / c)"
- by%unimportant (simp add: interval_lebesgue_integrable_def)
+ by (simp add: interval_lebesgue_integrable_def)
lemma interval_lebesgue_integral_mult_right [simp]:
fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
@@ -220,11 +220,11 @@
c * interval_lebesgue_integral M a b f"
by (simp add: interval_lebesgue_integral_def)
-lemma%important interval_lebesgue_integral_mult_left [simp]:
+lemma interval_lebesgue_integral_mult_left [simp]:
fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
shows "interval_lebesgue_integral M a b (\<lambda>x. f x * c) =
interval_lebesgue_integral M a b f * c"
- by%unimportant (simp add: interval_lebesgue_integral_def)
+ by (simp add: interval_lebesgue_integral_def)
lemma interval_lebesgue_integral_divide [simp]:
fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
@@ -242,11 +242,11 @@
unfolding interval_lebesgue_integral_def
by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real)
-lemma%important interval_lebesgue_integral_le_eq:
+lemma interval_lebesgue_integral_le_eq:
fixes a b f
assumes "a \<le> b"
shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
-using%unimportant assms by (auto simp: interval_lebesgue_integral_def)
+ using assms by (auto simp: interval_lebesgue_integral_def)
lemma interval_lebesgue_integral_gt_eq:
fixes a b f
@@ -271,9 +271,9 @@
interval_lebesgue_integrable lborel b a f"
by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same)
-lemma%important interval_integral_reflect:
+lemma interval_integral_reflect:
"(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
-proof%unimportant (induct a b rule: linorder_wlog)
+proof (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
split: if_split_asm)
@@ -299,7 +299,7 @@
lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\<infinity> | M. f x) = (LINT x : {a<..} | M. f x)"
unfolding interval_lebesgue_integral_def by auto
-lemma%important interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
+proposition interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
(set_integrable M {a<..} f)"
unfolding%unimportant interval_lebesgue_integrable_def by auto
@@ -317,12 +317,12 @@
unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
-lemma%important interval_integral_cong_AE:
+lemma interval_integral_cong_AE:
assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x"
shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
using assms
-proof%unimportant (induct a b rule: linorder_wlog)
+proof (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
next
@@ -331,11 +331,11 @@
intro!: set_lebesgue_integral_cong_AE)
qed
-lemma%important interval_integral_cong:
+lemma interval_integral_cong:
assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x"
shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
using assms
-proof%unimportant (induct a b rule: linorder_wlog)
+proof (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
next
@@ -407,11 +407,11 @@
apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
done
-lemma%important interval_integral_sum:
+lemma interval_integral_sum:
fixes a b c :: ereal
assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f"
shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)"
-proof%unimportant -
+proof -
let ?I = "\<lambda>a b. LBINT x=a..b. f x"
{ fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c"
then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f"
@@ -446,11 +446,11 @@
(simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
qed
-lemma%important interval_integrable_isCont:
+lemma interval_integrable_isCont:
fixes a b and f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
shows "(\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> isCont f x) \<Longrightarrow>
interval_lebesgue_integrable lborel a b f"
-proof%unimportant (induct a b rule: linorder_wlog)
+proof (induct a b rule: linorder_wlog)
case (le a b) then show ?case
unfolding interval_lebesgue_integrable_def set_integrable_def
by (auto simp: interval_lebesgue_integrable_def
@@ -478,7 +478,7 @@
subsection%important\<open>General limit approximation arguments\<close>
-lemma%important interval_integral_Icc_approx_nonneg:
+proposition interval_integral_Icc_approx_nonneg:
fixes a b :: ereal
assumes "a < b"
fixes u l :: "nat \<Rightarrow> real"
@@ -493,7 +493,7 @@
shows
"set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = C"
-proof%unimportant -
+proof -
have 1 [unfolded set_integrable_def]: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)"
proof -
@@ -534,7 +534,7 @@
by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
qed
-lemma%important interval_integral_Icc_approx_integrable:
+proposition interval_integral_Icc_approx_integrable:
fixes u l :: "nat \<Rightarrow> real" and a b :: ereal
fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
assumes "a < b"
@@ -543,7 +543,7 @@
"l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
assumes f_integrable: "set_integrable lborel (einterval a b) f"
shows "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
-proof%unimportant -
+proof -
have "(\<lambda>i. LBINT x:{l i.. u i}. f x) \<longlonglongrightarrow> (LBINT x:einterval a b. f x)"
unfolding set_lebesgue_integral_def
proof (rule integral_dominated_convergence)
@@ -580,13 +580,13 @@
TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
*)
-lemma%important interval_integral_FTC_finite:
+lemma interval_integral_FTC_finite:
fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
assumes f: "continuous_on {min a b..max a b} f"
assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within
{min a b..max a b})"
shows "(LBINT x=a..b. f x) = F b - F a"
-proof%unimportant (cases "a \<le> b")
+proof (cases "a \<le> b")
case True
have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)"
by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
@@ -617,7 +617,7 @@
qed
-lemma%important interval_integral_FTC_nonneg:
+lemma interval_integral_FTC_nonneg:
fixes f F :: "real \<Rightarrow> real" and a b :: ereal
assumes "a < b"
assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x"
@@ -628,7 +628,7 @@
shows
"set_integrable lborel (einterval a b) f"
"(LBINT x=a..b. f x) = B - A"
-proof%unimportant -
+proof -
obtain u l where approx:
"einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
@@ -669,7 +669,7 @@
by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
qed
-lemma%important interval_integral_FTC_integrable:
+theorem interval_integral_FTC_integrable:
fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal
assumes "a < b"
assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)"
@@ -678,7 +678,7 @@
assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
shows "(LBINT x=a..b. f x) = B - A"
-proof%unimportant -
+proof -
obtain u l where approx:
"einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
@@ -714,14 +714,14 @@
einterval.
*)
-lemma%important interval_integral_FTC2:
+theorem interval_integral_FTC2:
fixes a b c :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> c" "c \<le> b"
and contf: "continuous_on {a..b} f"
fixes x :: real
assumes "a \<le> x" and "x \<le> b"
shows "((\<lambda>u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})"
-proof%unimportant -
+proof -
let ?F = "(\<lambda>u. LBINT y=a..u. f y)"
have intf: "set_integrable lborel {a..b} f"
by (rule borel_integrable_atLeastAtMost', rule contf)
@@ -746,11 +746,11 @@
qed (insert assms, auto)
qed
-lemma%important einterval_antiderivative:
+proposition einterval_antiderivative:
fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x"
shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)"
-proof%unimportant -
+proof -
from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b"
by (auto simp: einterval_def)
let ?F = "(\<lambda>u. LBINT y=c..u. f y)"
@@ -786,14 +786,14 @@
text\<open>Once again, three versions: first, for finite intervals, and then two versions for
arbitrary intervals.\<close>
-lemma%important interval_integral_substitution_finite:
+theorem interval_integral_substitution_finite:
fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
assumes "a \<le> b"
and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})"
and contf : "continuous_on (g ` {a..b}) f"
and contg': "continuous_on {a..b} g'"
shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
-proof%unimportant-
+proof-
have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
using derivg unfolding has_field_derivative_iff_has_vector_derivative .
then have contg [simp]: "continuous_on {a..b} g"
@@ -833,7 +833,7 @@
(* TODO: is it possible to lift the assumption here that g' is nonnegative? *)
-lemma%important interval_integral_substitution_integrable:
+theorem interval_integral_substitution_integrable:
fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal
assumes "a < b"
and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
@@ -845,7 +845,7 @@
and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)"
shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
-proof%unimportant -
+proof -
obtain u l where approx [simp]:
"einterval a b = (\<Union>i. {l i .. u i})"
"incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
@@ -932,7 +932,7 @@
An alternative: make the second one the main one, and then have another lemma
that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *)
-lemma%important interval_integral_substitution_nonneg:
+theorem interval_integral_substitution_nonneg:
fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal
assumes "a < b"
and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
@@ -946,7 +946,7 @@
shows
"set_integrable lborel (einterval A B) f"
"(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
-proof%unimportant -
+proof -
from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
note less_imp_le [simp]
have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
@@ -1079,17 +1079,17 @@
translations
"CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
-lemma%important interval_integral_norm:
+proposition interval_integral_norm:
fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
using%unimportant integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
by%unimportant (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
-lemma%important interval_integral_norm2:
+proposition interval_integral_norm2:
"interval_lebesgue_integrable lborel a b f \<Longrightarrow>
norm (LBINT t=a..b. f t) \<le> \<bar>LBINT t=a..b. norm (f t)\<bar>"
-proof%unimportant (induct a b rule: linorder_wlog)
+proof (induct a b rule: linorder_wlog)
case (sym a b) then show ?case
by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
next