--- a/src/HOL/Analysis/Connected.thy Fri Dec 28 10:29:59 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy Fri Dec 28 18:53:19 2018 +0100
@@ -3519,7 +3519,7 @@
lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f"
by (force simp: homeomorphism_def)
-definition homeomorphic :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
+definition%important homeomorphic :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
(infixr "homeomorphic" 60)
where "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
--- a/src/HOL/Analysis/Continuous_Extension.thy Fri Dec 28 10:29:59 2018 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy Fri Dec 28 18:53:19 2018 +0100
@@ -297,10 +297,9 @@
using assms by (auto intro: Urysohn_local [of UNIV S T a b])
-subsection\<open>The Dugundji Extension Theorem and Tietze Variants\<close>
+subsection\<open>Dugundji's Extension Theorem and Tietze Variants\<close>
-text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
-https://projecteuclid.org/euclid.pjm/1103052106\<close>
+text \<open>See \cite{dugundji}.\<close>
theorem Dugundji:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
@@ -488,7 +487,7 @@
using assms
by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
-corollary Tietze_closed_interval:
+corollary%unimportant Tietze_closed_interval:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "continuous_on S f"
and "closedin (subtopology euclidean U) S"
@@ -499,7 +498,7 @@
apply (rule Dugundji [of "cbox a b" U S f])
using assms by auto
-corollary Tietze_closed_interval_1:
+corollary%unimportant Tietze_closed_interval_1:
fixes f :: "'a::euclidean_space \<Rightarrow> real"
assumes "continuous_on S f"
and "closedin (subtopology euclidean U) S"
@@ -510,7 +509,7 @@
apply (rule Dugundji [of "cbox a b" U S f])
using assms by (auto simp: image_subset_iff)
-corollary Tietze_open_interval:
+corollary%unimportant Tietze_open_interval:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "continuous_on S f"
and "closedin (subtopology euclidean U) S"
@@ -521,7 +520,7 @@
apply (rule Dugundji [of "box a b" U S f])
using assms by auto
-corollary Tietze_open_interval_1:
+corollary%unimportant Tietze_open_interval_1:
fixes f :: "'a::euclidean_space \<Rightarrow> real"
assumes "continuous_on S f"
and "closedin (subtopology euclidean U) S"
@@ -532,7 +531,7 @@
apply (rule Dugundji [of "box a b" U S f])
using assms by (auto simp: image_subset_iff)
-corollary Tietze_unbounded:
+corollary%unimportant Tietze_unbounded:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
assumes "continuous_on S f"
and "closedin (subtopology euclidean U) S"
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Dec 28 10:29:59 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Dec 28 18:53:19 2018 +0100
@@ -6,7 +6,7 @@
Author: Johannes Hoelzl, TU Muenchen
*)
-section \<open>Convex sets, functions and related things\<close>
+section \<open>Convex Sets and Functions\<close>
theory Convex_Euclidean_Space
imports
--- a/src/HOL/Analysis/Operator_Norm.thy Fri Dec 28 10:29:59 2018 +0100
+++ b/src/HOL/Analysis/Operator_Norm.thy Fri Dec 28 18:53:19 2018 +0100
@@ -3,7 +3,7 @@
Author: Brian Huffman
*)
-section%important \<open>Operator Norm\<close>
+section \<open>Operator Norm\<close>
theory Operator_Norm
imports Complex_Main
@@ -11,14 +11,15 @@
text \<open>This formulation yields zero if \<open>'a\<close> is the trivial vector space.\<close>
-definition%important onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real"
- where "onorm f = (SUP x. norm (f x) / norm x)"
+definition%important
+onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real" where
+"onorm f = (SUP x. norm (f x) / norm x)"
-lemma%important onorm_bound:
+proposition onorm_bound:
assumes "0 \<le> b" and "\<And>x. norm (f x) \<le> b * norm x"
shows "onorm f \<le> b"
unfolding onorm_def
-proof%unimportant (rule cSUP_least)
+proof (rule cSUP_least)
fix x
show "norm (f x) / norm x \<le> b"
using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq)
@@ -26,11 +27,11 @@
text \<open>In non-trivial vector spaces, the first assumption is redundant.\<close>
-lemma%important onorm_le:
+lemma onorm_le:
fixes f :: "'a::{real_normed_vector, perfect_space} \<Rightarrow> 'b::real_normed_vector"
assumes "\<And>x. norm (f x) \<le> b * norm x"
shows "onorm f \<le> b"
-proof%unimportant (rule onorm_bound [OF _ assms])
+proof (rule onorm_bound [OF _ assms])
have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
then obtain a :: 'a where "a \<noteq> 0" by fast
have "0 \<le> b * norm a"
@@ -39,10 +40,10 @@
by (simp add: zero_le_mult_iff)
qed
-lemma%important le_onorm:
+lemma le_onorm:
assumes "bounded_linear f"
shows "norm (f x) / norm x \<le> onorm f"
-proof%unimportant -
+proof -
interpret f: bounded_linear f by fact
obtain b where "0 \<le> b" and "\<forall>x. norm (f x) \<le> norm x * b"
using f.nonneg_bounded by auto
@@ -55,10 +56,10 @@
unfolding onorm_def by (rule cSUP_upper)
qed
-lemma%important onorm:
+lemma onorm:
assumes "bounded_linear f"
shows "norm (f x) \<le> onorm f * norm x"
-proof%unimportant -
+proof -
interpret f: bounded_linear f by fact
show ?thesis
proof (cases)
@@ -73,12 +74,12 @@
qed
qed
-lemma%unimportant onorm_pos_le:
+lemma onorm_pos_le:
assumes f: "bounded_linear f"
shows "0 \<le> onorm f"
using le_onorm [OF f, where x=0] by simp
-lemma%unimportant onorm_zero: "onorm (\<lambda>x. 0) = 0"
+lemma onorm_zero: "onorm (\<lambda>x. 0) = 0"
proof (rule order_antisym)
show "onorm (\<lambda>x. 0) \<le> 0"
by (simp add: onorm_bound)
@@ -86,20 +87,20 @@
using bounded_linear_zero by (rule onorm_pos_le)
qed
-lemma%unimportant onorm_eq_0:
+lemma onorm_eq_0:
assumes f: "bounded_linear f"
shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero)
-lemma%unimportant onorm_pos_lt:
+lemma onorm_pos_lt:
assumes f: "bounded_linear f"
shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)"
by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f])
-lemma%unimportant onorm_id_le: "onorm (\<lambda>x. x) \<le> 1"
+lemma onorm_id_le: "onorm (\<lambda>x. x) \<le> 1"
by (rule onorm_bound) simp_all
-lemma%unimportant onorm_id: "onorm (\<lambda>x. x::'a::{real_normed_vector, perfect_space}) = 1"
+lemma onorm_id: "onorm (\<lambda>x. x::'a::{real_normed_vector, perfect_space}) = 1"
proof (rule antisym[OF onorm_id_le])
have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
then obtain x :: 'a where "x \<noteq> 0" by fast
@@ -110,11 +111,11 @@
finally show "1 \<le> onorm (\<lambda>x::'a. x)" .
qed
-lemma%important onorm_compose:
+lemma onorm_compose:
assumes f: "bounded_linear f"
assumes g: "bounded_linear g"
shows "onorm (f \<circ> g) \<le> onorm f * onorm g"
-proof%unimportant (rule onorm_bound)
+proof (rule onorm_bound)
show "0 \<le> onorm f * onorm g"
by (intro mult_nonneg_nonneg onorm_pos_le f g)
next
@@ -127,7 +128,7 @@
by (simp add: mult.assoc)
qed
-lemma%unimportant onorm_scaleR_lemma:
+lemma onorm_scaleR_lemma:
assumes f: "bounded_linear f"
shows "onorm (\<lambda>x. r *\<^sub>R f x) \<le> \<bar>r\<bar> * onorm f"
proof (rule onorm_bound)
@@ -141,10 +142,10 @@
by (simp only: norm_scaleR mult.assoc)
qed
-lemma%important onorm_scaleR:
+lemma onorm_scaleR:
assumes f: "bounded_linear f"
shows "onorm (\<lambda>x. r *\<^sub>R f x) = \<bar>r\<bar> * onorm f"
-proof%unimportant (cases "r = 0")
+proof (cases "r = 0")
assume "r \<noteq> 0"
show ?thesis
proof (rule order_antisym)
@@ -160,7 +161,7 @@
qed
qed (simp add: onorm_zero)
-lemma%unimportant onorm_scaleR_left_lemma:
+lemma onorm_scaleR_left_lemma:
assumes r: "bounded_linear r"
shows "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
proof (rule onorm_bound)
@@ -173,10 +174,10 @@
by (simp add: ac_simps)
qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le r)
-lemma%important onorm_scaleR_left:
+lemma onorm_scaleR_left:
assumes f: "bounded_linear r"
shows "onorm (\<lambda>x. r x *\<^sub>R f) = onorm r * norm f"
-proof%unimportant (cases "f = 0")
+proof (cases "f = 0")
assume "f \<noteq> 0"
show ?thesis
proof (rule order_antisym)
@@ -200,15 +201,15 @@
qed
qed (simp add: onorm_zero)
-lemma%unimportant onorm_neg:
+lemma onorm_neg:
shows "onorm (\<lambda>x. - f x) = onorm f"
unfolding onorm_def by simp
-lemma%important onorm_triangle:
+lemma onorm_triangle:
assumes f: "bounded_linear f"
assumes g: "bounded_linear g"
shows "onorm (\<lambda>x. f x + g x) \<le> onorm f + onorm g"
-proof%unimportant (rule onorm_bound)
+proof (rule onorm_bound)
show "0 \<le> onorm f + onorm g"
by (intro add_nonneg_nonneg onorm_pos_le f g)
next
@@ -221,26 +222,26 @@
by (simp only: distrib_right)
qed
-lemma%important onorm_triangle_le:
+lemma onorm_triangle_le:
assumes "bounded_linear f"
assumes "bounded_linear g"
assumes "onorm f + onorm g \<le> e"
shows "onorm (\<lambda>x. f x + g x) \<le> e"
- using%unimportant assms by%unimportant (rule onorm_triangle [THEN order_trans])
+ using assms by (rule onorm_triangle [THEN order_trans])
-lemma%unimportant onorm_triangle_lt:
+lemma onorm_triangle_lt:
assumes "bounded_linear f"
assumes "bounded_linear g"
assumes "onorm f + onorm g < e"
shows "onorm (\<lambda>x. f x + g x) < e"
using assms by (rule onorm_triangle [THEN order_le_less_trans])
-lemma%important onorm_sum:
+lemma onorm_sum:
assumes "finite S"
assumes "\<And>s. s \<in> S \<Longrightarrow> bounded_linear (f s)"
shows "onorm (\<lambda>x. sum (\<lambda>s. f s x) S) \<le> sum (\<lambda>s. onorm (f s)) S"
- using%unimportant assms
- by%unimportant (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
+ using assms
+ by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
lemmas onorm_sum_le = onorm_sum[THEN order_trans]
--- a/src/HOL/Analysis/Path_Connected.thy Fri Dec 28 10:29:59 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Fri Dec 28 18:53:19 2018 +0100
@@ -2,7 +2,7 @@
Authors: LC Paulson and Robert Himmelmann (TU Muenchen), based on material from HOL Light
*)
-section \<open>Continuous Paths and Path-Connected Sets\<close>
+section \<open>Continuous Paths\<close>
theory Path_Connected
imports Continuous_Extension Continuum_Not_Denumerable
@@ -759,7 +759,7 @@
by (simp add: path_image_join sup_commute)
-section\<open>Choosing a subpath of an existing path\<close>
+subsection\<open>Subpath\<close>
definition%important subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
where "subpath a b g \<equiv> \<lambda>x. g((b - a) * x + a)"
@@ -1421,16 +1421,17 @@
by (rule_tac x="e/2" in exI) auto
qed
-
-section \<open>Path component\<close>
-
-text \<open>(by Tom Hales)\<close>
+section "Path-Connectedness" (* TODO: separate theory? *)
+
+subsection \<open>Path component\<close>
+
+text \<open>Original formalization by Tom Hales\<close>
definition%important "path_component s x y \<longleftrightarrow>
(\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
abbreviation%important
- "path_component_set s x \<equiv> Collect (path_component s x)"
+ "path_component_set s x \<equiv> Collect (path_component s x)"
lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def
@@ -3386,10 +3387,8 @@
qed
-section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps\<close>
-
-text%important\<open> We often just want to require that it fixes some subset, but to take in
- the case of a loop homotopy, it's convenient to have a general property P.\<close>
+section \<open>Homotopy of Maps\<close> (* TODO separate theory? *)
+
definition%important homotopic_with ::
"[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
@@ -3403,7 +3402,11 @@
(\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
-text\<open> We often want to just localize the ending function equality or whatever.\<close>
+text\<open>$p, q$ are functions $X \to Y$, and the property $P$ restricts all intermediate maps.
+We often just want to require that $P$ fixes some subset, but to include the case of a loop homotopy,
+it is convenient to have a general property $P$.\<close>
+
+text \<open>We often want to just localize the ending function equality or whatever.\<close>
proposition homotopic_with:
fixes X :: "'a::topological_space set" and Y :: "'b::topological_space set"
assumes "\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
@@ -7463,7 +7466,7 @@
-subsection\<open>Self-homeomorphisms shuffling points about\<close>
+subsection%unimportant \<open>Self-homeomorphisms shuffling points about\<close>
subsubsection%unimportant\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
@@ -7595,7 +7598,7 @@
done
qed
-corollary homeomorphism_moving_point_2:
+corollary%unimportant homeomorphism_moving_point_2:
fixes a :: "'a::euclidean_space"
assumes "affine T" "a \<in> T" and u: "u \<in> ball a r \<inter> T" and v: "v \<in> ball a r \<inter> T"
obtains f g where "homeomorphism (cball a r \<inter> T) (cball a r \<inter> T) f g"
@@ -7623,7 +7626,7 @@
qed
-corollary homeomorphism_moving_point_3:
+corollary%unimportant homeomorphism_moving_point_3:
fixes a :: "'a::euclidean_space"
assumes "affine T" "a \<in> T" and ST: "ball a r \<inter> T \<subseteq> S" "S \<subseteq> T"
and u: "u \<in> ball a r \<inter> T" and v: "v \<in> ball a r \<inter> T"
@@ -7701,7 +7704,7 @@
qed
-proposition homeomorphism_moving_point:
+proposition%unimportant homeomorphism_moving_point:
fixes a :: "'a::euclidean_space"
assumes ope: "openin (subtopology euclidean (affine hull S)) S"
and "S \<subseteq> T"
@@ -7857,7 +7860,7 @@
qed
qed
-proposition homeomorphism_moving_points_exists:
+proposition%unimportant homeomorphism_moving_points_exists:
fixes S :: "'a::euclidean_space set"
assumes 2: "2 \<le> DIM('a)" "open S" "connected S" "S \<subseteq> T" "finite K"
and KS: "\<And>i. i \<in> K \<Longrightarrow> x i \<in> S \<and> y i \<in> S"
@@ -8123,7 +8126,7 @@
qed
qed
-proposition homeomorphism_grouping_points_exists:
+proposition%unimportant homeomorphism_grouping_points_exists:
fixes S :: "'a::euclidean_space set"
assumes "open U" "open S" "connected S" "U \<noteq> {}" "finite K" "K \<subseteq> S" "U \<subseteq> S" "S \<subseteq> T"
obtains f g where "homeomorphism T T f g" "{x. (\<not> (f x = x \<and> g x = x))} \<subseteq> S"
@@ -8202,7 +8205,7 @@
qed
-proposition homeomorphism_grouping_points_exists_gen:
+proposition%unimportant homeomorphism_grouping_points_exists_gen:
fixes S :: "'a::euclidean_space set"
assumes opeU: "openin (subtopology euclidean S) U"
and opeS: "openin (subtopology euclidean (affine hull S)) S"
--- a/src/HOL/Analysis/Starlike.thy Fri Dec 28 10:29:59 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy Fri Dec 28 18:53:19 2018 +0100
@@ -6,10 +6,10 @@
Author: Johannes Hoelzl, TU Muenchen
*)
-section \<open>Line segments, Starlike Sets, etc\<close>
+section \<open>Line Segments\<close>
theory Starlike
- imports Convex_Euclidean_Space
+imports Convex_Euclidean_Space
begin
subsection \<open>Midpoint\<close>
--- a/src/HOL/Analysis/document/root.tex Fri Dec 28 10:29:59 2018 +0100
+++ b/src/HOL/Analysis/document/root.tex Fri Dec 28 18:53:19 2018 +0100
@@ -31,4 +31,9 @@
\parindent 0pt\parskip 0.5ex
\input{session}
+\pagestyle{headings}
+\bibliographystyle{abbrv}
+\bibliography{root}
+\nocite{dummy}
+
\end{document}
--- a/src/HOL/ROOT Fri Dec 28 10:29:59 2018 +0100
+++ b/src/HOL/ROOT Fri Dec 28 18:53:19 2018 +0100
@@ -69,6 +69,7 @@
Analysis
document_files
"root.tex"
+ "root.bib"
session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
theories