--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Fri Apr 06 17:34:50 2018 +0200
@@ -468,6 +468,12 @@
text\<open>Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"}\<close>
+definition 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)"
+ by (simp add: map_matrix_def)
+
definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m"
(infixl "**" 70)
where "m ** m' == (\<chi> i j. sum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
--- a/src/HOL/Analysis/Connected.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Connected.thy Fri Apr 06 17:34:50 2018 +0200
@@ -8,7 +8,7 @@
imports Topology_Euclidean_Space
begin
-subsection \<open>More properties of closed balls, spheres, etc.\<close>
+subsection%unimportant \<open>More properties of closed balls, spheres, etc.\<close>
lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
apply (simp add: interior_def, safe)
@@ -345,7 +345,7 @@
shows "closed (sphere a r)"
by (simp add: compact_imp_closed)
-subsection \<open>Connectedness\<close>
+subsection%unimportant \<open>Connectedness\<close>
lemma connected_local:
"connected S \<longleftrightarrow>
@@ -410,7 +410,7 @@
subsection \<open>Connected components, considered as a connectedness relation or a set\<close>
-definition "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
+definition%important "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
abbreviation "connected_component_set s x \<equiv> Collect (connected_component s x)"
@@ -610,7 +610,7 @@
subsection \<open>The set of connected components of a set\<close>
-definition components:: "'a::topological_space set \<Rightarrow> 'a set set"
+definition%important components:: "'a::topological_space set \<Rightarrow> 'a set set"
where "components s \<equiv> connected_component_set s ` s"
lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
@@ -776,12 +776,12 @@
subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
-proposition bounded_closed_chain:
+proposition%important bounded_closed_chain:
fixes \<F> :: "'a::heine_borel set set"
assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
shows "\<Inter>\<F> \<noteq> {}"
-proof -
+proof%unimportant -
have "B \<inter> \<Inter>\<F> \<noteq> {}"
proof (rule compact_imp_fip)
show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
@@ -824,12 +824,12 @@
then show ?thesis by blast
qed
-corollary compact_chain:
+corollary%important compact_chain:
fixes \<F> :: "'a::heine_borel set set"
assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
"\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
shows "\<Inter> \<F> \<noteq> {}"
-proof (cases "\<F> = {}")
+proof%unimportant (cases "\<F> = {}")
case True
then show ?thesis by auto
next
@@ -852,12 +852,12 @@
qed
text\<open>The Baire property of dense sets\<close>
-theorem Baire:
+theorem%important Baire:
fixes S::"'a::{real_normed_vector,heine_borel} set"
assumes "closed S" "countable \<G>"
and ope: "\<And>T. T \<in> \<G> \<Longrightarrow> openin (subtopology euclidean S) T \<and> S \<subseteq> closure T"
shows "S \<subseteq> closure(\<Inter>\<G>)"
-proof (cases "\<G> = {}")
+proof%unimportant (cases "\<G> = {}")
case True
then show ?thesis
using closure_subset by auto
@@ -961,7 +961,7 @@
qed
qed
-subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
+subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded".\<close>
lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
by (simp add: bounded_iff)
@@ -1139,7 +1139,7 @@
qed
-subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
+subsection%unimportant\<open>Relations among convergence and absolute convergence for power series.\<close>
lemma summable_imp_bounded:
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
@@ -1166,7 +1166,7 @@
done
qed
-subsection \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
+subsection%unimportant \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
lemma bounded_closed_nest:
fixes s :: "nat \<Rightarrow> ('a::heine_borel) set"
@@ -1286,7 +1286,7 @@
subsection \<open>Infimum Distance\<close>
-definition "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
+definition%important "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
by (auto intro!: zero_le_dist)
@@ -1515,7 +1515,7 @@
by (simp add: compact_eq_bounded_closed)
qed
-subsection \<open>Equality of continuous functions on closure and related results.\<close>
+subsection%unimportant \<open>Equality of continuous functions on closure and related results.\<close>
lemma continuous_closedin_preimage_constant:
fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -1618,7 +1618,7 @@
qed
qed
-subsection \<open>A function constant on a set\<close>
+subsection%unimportant \<open>A function constant on a set\<close>
definition constant_on (infixl "(constant'_on)" 50)
where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
@@ -1639,7 +1639,7 @@
using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
by metis
-subsection\<open>Relating linear images to open/closed/interior/closure\<close>
+subsection%unimportant\<open>Relating linear images to open/closed/interior/closure\<close>
proposition open_surjective_linear_image:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
@@ -1786,7 +1786,7 @@
qed
qed
-subsection\<open> Theorems relating continuity and uniform continuity to closures\<close>
+subsection%unimportant\<open> Theorems relating continuity and uniform continuity to closures\<close>
lemma continuous_on_closure:
"continuous_on (closure S) f \<longleftrightarrow>
@@ -2047,7 +2047,7 @@
shows "bounded(f ` S)"
by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
-subsection \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
+subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
lemma continuous_within_avoid:
fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
@@ -2097,7 +2097,7 @@
using continuous_at_avoid[of x f a] assms(4)
by auto
-subsection\<open>Quotient maps\<close>
+subsection%unimportant\<open>Quotient maps\<close>
lemma quotient_map_imp_continuous_open:
assumes T: "f ` S \<subseteq> T"
@@ -2447,15 +2447,15 @@
ultimately show ?thesis using that by blast
qed
-corollary compact_uniformly_continuous:
+corollary%important compact_uniformly_continuous:
fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
assumes f: "continuous_on S f" and S: "compact S"
shows "uniformly_continuous_on S f"
- using f
+ using%unimportant f
unfolding continuous_on_iff uniformly_continuous_on_def
by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])
-subsection \<open>Topological stuff about the set of Reals\<close>
+subsection%unimportant \<open>Topological stuff about the set of Reals\<close>
lemma open_real:
fixes s :: "real set"
@@ -2492,7 +2492,7 @@
unfolding continuous_on_iff dist_norm by simp
-subsection \<open>Cartesian products\<close>
+subsection%unimportant \<open>Cartesian products\<close>
lemma bounded_Times:
assumes "bounded s" "bounded t"
@@ -2668,7 +2668,7 @@
subsection \<open>The diameter of a set.\<close>
-definition diameter :: "'a::metric_space set \<Rightarrow> real" where
+definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where
"diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
lemma diameter_empty [simp]: "diameter{} = 0"
@@ -2933,11 +2933,11 @@
subsection \<open>Separation between points and sets\<close>
-lemma separate_point_closed:
+lemma%important separate_point_closed:
fixes s :: "'a::heine_borel set"
assumes "closed s" and "a \<notin> s"
shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"
-proof (cases "s = {}")
+proof%unimportant (cases "s = {}")
case True
then show ?thesis by(auto intro!: exI[where x=1])
next
@@ -2948,12 +2948,12 @@
by blast
qed
-lemma separate_compact_closed:
+lemma%important separate_compact_closed:
fixes s t :: "'a::heine_borel set"
assumes "compact s"
and t: "closed t" "s \<inter> t = {}"
shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof cases
+proof%unimportant cases
assume "s \<noteq> {} \<and> t \<noteq> {}"
then have "s \<noteq> {}" "t \<noteq> {}" by auto
let ?inf = "\<lambda>x. infdist x t"
@@ -2968,27 +2968,27 @@
ultimately show ?thesis by auto
qed (auto intro!: exI[of _ 1])
-lemma separate_closed_compact:
+lemma%important separate_closed_compact:
fixes s t :: "'a::heine_borel set"
assumes "closed s"
and "compact t"
and "s \<inter> t = {}"
shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof -
+proof%unimportant -
have *: "t \<inter> s = {}"
using assms(3) by auto
show ?thesis
using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
qed
-lemma compact_in_open_separated:
+lemma%important compact_in_open_separated:
fixes A::"'a::heine_borel set"
assumes "A \<noteq> {}"
assumes "compact A"
assumes "open B"
assumes "A \<subseteq> B"
obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
-proof atomize_elim
+proof%unimportant atomize_elim
have "closed (- B)" "compact A" "- B \<inter> A = {}"
using assms by (auto simp: open_Diff compact_eq_bounded_closed)
from separate_closed_compact[OF this]
@@ -3014,7 +3014,7 @@
qed
-subsection \<open>Compact sets and the closure operation.\<close>
+subsection%unimportant \<open>Compact sets and the closure operation.\<close>
lemma closed_scaling:
fixes S :: "'a::real_normed_vector set"
@@ -3165,7 +3165,7 @@
done
-subsection \<open>Closure of halfspaces and hyperplanes\<close>
+subsection%unimportant \<open>Closure of halfspaces and hyperplanes\<close>
lemma continuous_on_closed_Collect_le:
fixes f g :: "'a::t2_space \<Rightarrow> real"
@@ -3492,7 +3492,7 @@
subsection \<open>Homeomorphisms\<close>
-definition "homeomorphism s t f g \<longleftrightarrow>
+definition%important "homeomorphism s t f g \<longleftrightarrow>
(\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
(\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
@@ -3812,7 +3812,7 @@
using assms unfolding homeomorphic_def homeomorphism_def by (metis connected_continuous_image)
-subsection\<open>Inverse function property for open/closed maps\<close>
+subsection%unimportant\<open>Inverse function property for open/closed maps\<close>
lemma continuous_on_inverse_open_map:
assumes contf: "continuous_on S f"
@@ -3963,12 +3963,12 @@
unfolding complete_def by auto
qed
-lemma injective_imp_isometric:
+lemma%important injective_imp_isometric:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes s: "closed s" "subspace s"
and f: "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0"
shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm x"
-proof (cases "s \<subseteq> {0::'a}")
+proof%unimportant (cases "s \<subseteq> {0::'a}")
case True
have "norm x \<le> norm (f x)" if "x \<in> s" for x
proof -
@@ -4036,11 +4036,11 @@
ultimately show ?thesis by auto
qed
-lemma closed_injective_image_subspace:
+lemma%important closed_injective_image_subspace:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 \<longrightarrow> x = 0" "closed s"
shows "closed(f ` s)"
-proof -
+proof%unimportant -
obtain e where "e > 0" and e: "\<forall>x\<in>s. e * norm x \<le> norm (f x)"
using injective_imp_isometric[OF assms(4,1,2,3)] by auto
show ?thesis
@@ -4049,7 +4049,7 @@
qed
-subsection \<open>Some properties of a canonical subspace\<close>
+subsection%unimportant \<open>Some properties of a canonical subspace\<close>
lemma subspace_substandard: "subspace {x::'a::euclidean_space. (\<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0)}"
by (auto simp: subspace_def inner_add_left)
@@ -4157,7 +4157,7 @@
qed
-subsection \<open>Affine transformations of intervals\<close>
+subsection%unimportant \<open>Affine transformations of intervals\<close>
lemma real_affinity_le: "0 < m \<Longrightarrow> m * x + c \<le> y \<longleftrightarrow> x \<le> inverse m * y + - (c / m)"
for m :: "'a::linordered_field"
@@ -4186,13 +4186,13 @@
subsection \<open>Banach fixed point theorem (not really topological ...)\<close>
-theorem banach_fix:
+theorem%important banach_fix:
assumes s: "complete s" "s \<noteq> {}"
and c: "0 \<le> c" "c < 1"
and f: "f ` s \<subseteq> s"
and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
shows "\<exists>!x\<in>s. f x = x"
-proof -
+proof%unimportant -
from c have "1 - c > 0" by simp
from s(2) obtain z0 where z0: "z0 \<in> s" by blast
@@ -4342,13 +4342,13 @@
subsection \<open>Edelstein fixed point theorem\<close>
-theorem edelstein_fix:
+theorem%important edelstein_fix:
fixes s :: "'a::metric_space set"
assumes s: "compact s" "s \<noteq> {}"
and gs: "(g ` s) \<subseteq> s"
and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
shows "\<exists>!x\<in>s. g x = x"
-proof -
+proof%unimportant -
let ?D = "(\<lambda>x. (x, x)) ` s"
have D: "compact ?D" "?D \<noteq> {}"
by (rule compact_continuous_image)
@@ -4697,10 +4697,10 @@
done
qed
-proposition separable:
+proposition%important separable:
fixes S :: "'a:: euclidean_space set"
obtains T where "countable T" "T \<subseteq> S" "S \<subseteq> closure T"
-proof -
+proof%unimportant -
obtain \<B> :: "'a:: euclidean_space set set"
where "countable \<B>"
and "{} \<notin> \<B>"
@@ -4743,11 +4743,11 @@
qed
qed
-proposition Lindelof:
+proposition%important Lindelof:
fixes \<F> :: "'a::euclidean_space set set"
assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
-proof -
+proof%unimportant -
obtain \<B> :: "'a set set"
where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
@@ -5049,11 +5049,11 @@
qed
-proposition component_diff_connected:
+proposition%important component_diff_connected:
fixes S :: "'a::metric_space set"
assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
shows "connected(U - C)"
- using \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
+ using%unimportant \<open>connected S\<close> unfolding connected_closedin_eq not_ex de_Morgan_conj
proof clarify
fix H3 H4
assume clo3: "closedin (subtopology euclidean (U - C)) H3"
@@ -5093,7 +5093,7 @@
by auto
qed
-subsection\<open> Finite intersection property\<close>
+subsection%unimportant\<open> Finite intersection property\<close>
text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
@@ -5149,7 +5149,7 @@
by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)
-subsection\<open>Componentwise limits and continuity\<close>
+subsection%unimportant\<open>Componentwise limits and continuity\<close>
text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
@@ -5179,11 +5179,11 @@
by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
qed
-proposition tendsto_componentwise_iff:
+proposition%important tendsto_componentwise_iff:
fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
(is "?lhs = ?rhs")
-proof
+proof%unimportant
assume ?lhs
then show ?rhs
unfolding tendsto_def
@@ -5267,9 +5267,9 @@
by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
qed
-subsection\<open>Pasting functions together\<close>
-
-subsubsection\<open>on open sets\<close>
+subsection%unimportant\<open>Pasting functions together\<close>
+
+subsubsection%unimportant\<open>on open sets\<close>
lemma pasting_lemma:
fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
@@ -5311,7 +5311,7 @@
by (metis (no_types, lifting) IntD2 IntI f someI_ex)
qed
-subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close>
+subsubsection%unimportant\<open>Likewise on closed sets, with a finiteness assumption\<close>
lemma pasting_lemma_closed:
fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::topological_space"
@@ -5436,7 +5436,7 @@
qed
-subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
+subsection%unimportant\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
@@ -5595,7 +5595,7 @@
-subsection \<open>Continuous Extension\<close>
+subsection%unimportant \<open>Continuous Extension\<close>
definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
"clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
--- a/src/HOL/Analysis/Continuous_Extension.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Continuous_Extension.thy Fri Apr 06 17:34:50 2018 +0200
@@ -13,7 +13,7 @@
text\<open>A difference from HOL Light: all summations over infinite sets equal zero,
so the "support" must be made explicit in the summation below!\<close>
-proposition subordinate_partition_of_unity:
+proposition%important subordinate_partition_of_unity:
fixes S :: "'a :: euclidean_space set"
assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
@@ -22,7 +22,7 @@
and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
and "\<And>x. x \<in> S \<Longrightarrow> supp_sum (\<lambda>W. F W x) \<C> = 1"
and "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}"
-proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
+proof%unimportant (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
case True
then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
then show ?thesis
@@ -283,7 +283,7 @@
"\<And>x. f x = b \<longleftrightarrow> x \<in> T"
using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
-proposition Urysohn:
+proposition%important Urysohn:
assumes US: "closed S"
and UT: "closed T"
and "S \<inter> T = {}"
@@ -292,22 +292,22 @@
"\<And>x. f x \<in> closed_segment a b"
"\<And>x. x \<in> S \<Longrightarrow> f x = a"
"\<And>x. x \<in> T \<Longrightarrow> f x = b"
-using assms by (auto intro: Urysohn_local [of UNIV S T a b])
+using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b])
subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close>
-text\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
+text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
http://projecteuclid.org/euclid.pjm/1103052106\<close>
-theorem Dugundji:
+theorem%important Dugundji:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
assumes "convex C" "C \<noteq> {}"
and cloin: "closedin (subtopology euclidean U) S"
and contf: "continuous_on S f" and "f ` S \<subseteq> C"
obtains g where "continuous_on U g" "g ` U \<subseteq> C"
"\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof (cases "S = {}")
+proof%unimportant (cases "S = {}")
case True then show thesis
apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
apply (rule continuous_intros)
@@ -475,7 +475,7 @@
qed
-corollary Tietze:
+corollary%important Tietze:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
assumes "continuous_on S f"
and "closedin (subtopology euclidean U) S"
@@ -483,7 +483,7 @@
and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
"\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
-using assms
+using%unimportant assms
by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
corollary Tietze_closed_interval:
--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy Fri Apr 06 17:34:50 2018 +0200
@@ -11,7 +11,7 @@
"HOL-Library.Countable_Set"
begin
-subsection \<open>Abstract\<close>
+subsection%unimportant \<open>Abstract\<close>
text \<open>
The following document presents a proof that the Continuum is uncountable.
@@ -33,8 +33,8 @@
Nested Interval Property.
\<close>
-theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
-proof
+theorem%important real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
+proof%unimportant
assume "\<exists>f::nat \<Rightarrow> real. surj f"
then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Apr 06 17:34:50 2018 +0200
@@ -177,7 +177,7 @@
subsection \<open>Convexity\<close>
-definition convex :: "'a::real_vector set \<Rightarrow> bool"
+definition%important convex :: "'a::real_vector set \<Rightarrow> bool"
where "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
lemma convexI:
@@ -350,7 +350,7 @@
by (simp add: convex_def scaleR_conv_of_real)
-subsection \<open>Explicit expressions for convexity in terms of arbitrary sums\<close>
+subsection%unimportant \<open>Explicit expressions for convexity in terms of arbitrary sums\<close>
lemma convex_sum:
fixes C :: "'a::real_vector set"
@@ -503,7 +503,7 @@
subsection \<open>Functions that are convex on a set\<close>
-definition convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
+definition%important convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
where "convex_on s f \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
@@ -624,7 +624,7 @@
qed
-subsection \<open>Arithmetic operations on sets preserve convexity\<close>
+subsection%unimportant \<open>Arithmetic operations on sets preserve convexity\<close>
lemma convex_linear_image:
assumes "linear f"
@@ -1087,7 +1087,7 @@
qed
-subsection \<open>Convexity of real functions\<close>
+subsection%unimportant \<open>Convexity of real functions\<close>
lemma convex_on_realI:
assumes "connected A"
@@ -1406,7 +1406,7 @@
subsection \<open>Affine set and affine hull\<close>
-definition affine :: "'a::real_vector set \<Rightarrow> bool"
+definition%important affine :: "'a::real_vector set \<Rightarrow> bool"
where "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
@@ -1444,7 +1444,7 @@
by (simp add: affine_def algebra_simps) (metis distrib_right mult.left_neutral)
-subsubsection \<open>Some explicit formulations (from Lars Schewe)\<close>
+subsubsection%unimportant \<open>Some explicit formulations (from Lars Schewe)\<close>
lemma affine:
fixes V::"'a::real_vector set"
@@ -1668,7 +1668,7 @@
qed
-subsubsection \<open>Stepping theorems and hence small special cases\<close>
+subsubsection%unimportant \<open>Stepping theorems and hence small special cases\<close>
lemma affine_hull_empty[simp]: "affine hull {} = {}"
by (rule hull_unique) auto
@@ -1806,7 +1806,7 @@
by (metis add_uminus_conv_diff mem_affine_3_minus real_vector.scale_minus_left)
-subsubsection \<open>Some relations between affine hull and subspaces\<close>
+subsubsection%unimportant \<open>Some relations between affine hull and subspaces\<close>
lemma affine_hull_insert_subset_span:
"affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
@@ -1867,7 +1867,7 @@
using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
-subsubsection \<open>Parallel affine sets\<close>
+subsubsection%unimportant \<open>Parallel affine sets\<close>
definition affine_parallel :: "'a::real_vector set \<Rightarrow> 'a::real_vector set \<Rightarrow> bool"
where "affine_parallel S T \<longleftrightarrow> (\<exists>a. T = (\<lambda>x. a + x) ` S)"
@@ -1974,7 +1974,7 @@
unfolding subspace_def affine_def by auto
-subsubsection \<open>Subspace parallel to an affine set\<close>
+subsubsection%unimportant \<open>Subspace parallel to an affine set\<close>
lemma subspace_affine: "subspace S \<longleftrightarrow> affine S \<and> 0 \<in> S"
proof -
@@ -2100,7 +2100,7 @@
subsection \<open>Cones\<close>
-definition cone :: "'a::real_vector set \<Rightarrow> bool"
+definition%important cone :: "'a::real_vector set \<Rightarrow> bool"
where "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. c *\<^sub>R x \<in> s)"
lemma cone_empty[intro, simp]: "cone {}"
@@ -2214,9 +2214,9 @@
shows "c *\<^sub>R x \<in> cone hull S"
by (metis assms cone_cone_hull hull_inc mem_cone)
-lemma cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
+lemma%important cone_hull_expl: "cone hull S = {c *\<^sub>R x | c x. c \<ge> 0 \<and> x \<in> S}"
(is "?lhs = ?rhs")
-proof -
+proof%unimportant -
{
fix x
assume "x \<in> ?rhs"
@@ -2282,7 +2282,7 @@
subsection \<open>Affine dependence and consequential theorems (from Lars Schewe)\<close>
-definition affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
+definition%important affine_dependent :: "'a::real_vector set \<Rightarrow> bool"
where "affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> affine hull (s - {x}))"
lemma affine_dependent_subset:
@@ -2299,11 +2299,11 @@
"~ affine_dependent s \<Longrightarrow> ~ affine_dependent(s - t)"
by (meson Diff_subset affine_dependent_subset)
-lemma affine_dependent_explicit:
+lemma%important affine_dependent_explicit:
"affine_dependent p \<longleftrightarrow>
(\<exists>s u. finite s \<and> s \<subseteq> p \<and> sum u s = 0 \<and>
(\<exists>v\<in>s. u v \<noteq> 0) \<and> sum (\<lambda>v. u v *\<^sub>R v) s = 0)"
- unfolding affine_dependent_def affine_hull_explicit mem_Collect_eq
+ unfolding%unimportant affine_dependent_def affine_hull_explicit mem_Collect_eq
apply rule
apply (erule bexE, erule exE, erule exE)
apply (erule conjE)+
@@ -2365,7 +2365,7 @@
qed
-subsection \<open>Connectedness of convex sets\<close>
+subsection%unimportant \<open>Connectedness of convex sets\<close>
lemma connectedD:
"connected S \<Longrightarrow> open A \<Longrightarrow> open B \<Longrightarrow> S \<subseteq> A \<union> B \<Longrightarrow> A \<inter> B \<inter> S = {} \<Longrightarrow> A \<inter> S = {} \<or> B \<inter> S = {}"
@@ -2558,7 +2558,7 @@
by auto
-subsubsection \<open>Convex hull is "preserved" by a linear function\<close>
+subsubsection%unimportant \<open>Convex hull is "preserved" by a linear function\<close>
lemma convex_hull_linear_image:
assumes f: "linear f"
@@ -2616,7 +2616,7 @@
qed
-subsubsection \<open>Stepping theorems for convex hulls of finite sets\<close>
+subsubsection%unimportant \<open>Stepping theorems for convex hulls of finite sets\<close>
lemma convex_hull_empty[simp]: "convex hull {} = {}"
by (rule hull_unique) auto
@@ -2742,16 +2742,16 @@
using diff_eq_eq apply fastforce
by (metis add.group_left_neutral add_le_imp_le_diff diff_add_cancel)
-subsubsection \<open>Explicit expression for convex hull\<close>
-
-lemma convex_hull_indexed:
+subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
+
+lemma%important convex_hull_indexed:
fixes s :: "'a::real_vector set"
shows "convex hull s =
{y. \<exists>k u x.
(\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
(sum u {1..k} = 1) \<and> (sum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}"
(is "?xyz = ?hull")
- apply (rule hull_unique)
+ apply%unimportant (rule hull_unique)
apply rule
defer
apply (rule convexI)
@@ -2887,7 +2887,7 @@
qed
-subsubsection \<open>Another formulation from Lars Schewe\<close>
+subsubsection%unimportant \<open>Another formulation from Lars Schewe\<close>
lemma convex_hull_explicit:
fixes p :: "'a::real_vector set"
@@ -2991,7 +2991,7 @@
qed
-subsubsection \<open>A stepping theorem for that expansion\<close>
+subsubsection%unimportant \<open>A stepping theorem for that expansion\<close>
lemma convex_hull_finite_step:
fixes s :: "'a::real_vector set"
@@ -3061,7 +3061,7 @@
qed
-subsubsection \<open>Hence some special cases\<close>
+subsubsection%unimportant \<open>Hence some special cases\<close>
lemma convex_hull_2:
"convex hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b | u v. 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1}"
@@ -3141,7 +3141,7 @@
qed
-subsection \<open>Relations among closure notions and corresponding hulls\<close>
+subsection%unimportant \<open>Relations among closure notions and corresponding hulls\<close>
lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
unfolding affine_def convex_def by auto
@@ -3306,7 +3306,7 @@
qed
-subsection \<open>Some Properties of Affine Dependent Sets\<close>
+subsection%unimportant \<open>Some Properties of Affine Dependent Sets\<close>
lemma affine_independent_0 [simp]: "\<not> affine_dependent {}"
by (simp add: affine_dependent_def)
@@ -3546,7 +3546,7 @@
subsection \<open>Affine Dimension of a Set\<close>
-definition aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
+definition%important aff_dim :: "('a::euclidean_space) set \<Rightarrow> int"
where "aff_dim V =
(SOME d :: int.
\<exists>B. affine hull B = affine hull V \<and> \<not> affine_dependent B \<and> of_nat (card B) = d + 1)"
@@ -4417,11 +4417,11 @@
by (auto simp add: convex_hull_explicit)
qed
-theorem caratheodory:
+theorem%important caratheodory:
"convex hull p =
{x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
-proof safe
+proof%unimportant safe
fix x
assume "x \<in> convex hull p"
then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
@@ -4444,7 +4444,7 @@
subsection \<open>Relative interior of a set\<close>
-definition "rel_interior S =
+definition%important "rel_interior S =
{x. \<exists>T. openin (subtopology euclidean (affine hull S)) T \<and> x \<in> T \<and> T \<subseteq> S}"
lemma rel_interior_mono:
@@ -4769,7 +4769,7 @@
subsubsection \<open>Relative open sets\<close>
-definition "rel_open S \<longleftrightarrow> rel_interior S = S"
+definition%important "rel_open S \<longleftrightarrow> rel_interior S = S"
lemma rel_open: "rel_open S \<longleftrightarrow> openin (subtopology euclidean (affine hull S)) S"
unfolding rel_open_def rel_interior_def
@@ -4970,7 +4970,7 @@
qed
-subsubsection\<open>Relative interior preserves under linear transformations\<close>
+subsubsection%unimportant\<open>Relative interior preserves under linear transformations\<close>
lemma rel_interior_translation_aux:
fixes a :: "'n::euclidean_space"
@@ -5134,7 +5134,7 @@
by auto
-subsection\<open>Some Properties of subset of standard basis\<close>
+subsection%unimportant\<open>Some Properties of subset of standard basis\<close>
lemma affine_hull_substd_basis:
assumes "d \<subseteq> Basis"
@@ -5151,7 +5151,7 @@
by (metis Int_absorb1 Int_absorb2 convex_hull_subset_affine_hull hull_hull hull_mono hull_subset)
-subsection \<open>Openness and compactness are preserved by convex hull operation.\<close>
+subsection%unimportant \<open>Openness and compactness are preserved by convex hull operation.\<close>
lemma open_convex_hull[intro]:
fixes s :: "'a::real_normed_vector set"
@@ -5422,7 +5422,7 @@
qed
-subsection \<open>Extremal points of a simplex are some vertices.\<close>
+subsection%unimportant \<open>Extremal points of a simplex are some vertices.\<close>
lemma dist_increases_online:
fixes a b d :: "'a::real_inner"
@@ -5623,7 +5623,7 @@
subsection \<open>Closest point of a convex set is unique, with a continuous projection.\<close>
-definition closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
+definition%important closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
where "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
lemma closest_point_exists:
@@ -5811,7 +5811,7 @@
qed
-subsubsection \<open>Various point-to-set separating/supporting hyperplane theorems.\<close>
+subsubsection%unimportant \<open>Various point-to-set separating/supporting hyperplane theorems.\<close>
lemma supporting_hyperplane_closed_point:
fixes z :: "'a::{real_inner,heine_borel}"
@@ -5933,7 +5933,7 @@
qed
-subsubsection \<open>Now set-to-set for closed/compact sets\<close>
+subsubsection%unimportant \<open>Now set-to-set for closed/compact sets\<close>
lemma separating_hyperplane_closed_compact:
fixes S :: "'a::euclidean_space set"
@@ -6024,7 +6024,7 @@
qed
-subsubsection \<open>General case without assuming closure and getting non-strict separation\<close>
+subsubsection%unimportant \<open>General case without assuming closure and getting non-strict separation\<close>
lemma separating_hyperplane_set_0:
assumes "convex s" "(0::'a::euclidean_space) \<notin> s"
@@ -6082,7 +6082,7 @@
qed
-subsection \<open>More convexity generalities\<close>
+subsection%unimportant \<open>More convexity generalities\<close>
lemma convex_closure [intro,simp]:
fixes s :: "'a::real_normed_vector set"
@@ -6132,7 +6132,7 @@
using hull_subset[of s convex] convex_hull_empty by auto
-subsection \<open>Moving and scaling convex hulls.\<close>
+subsection%unimportant \<open>Moving and scaling convex hulls.\<close>
lemma convex_hull_set_plus:
"convex hull (s + t) = convex hull s + convex hull t"
@@ -6159,7 +6159,7 @@
by(simp only: image_image[symmetric] convex_hull_scaling convex_hull_translation)
-subsection \<open>Convexity of cone hulls\<close>
+subsection%unimportant \<open>Convexity of cone hulls\<close>
lemma convex_cone_hull:
assumes "convex S"
@@ -6227,7 +6227,7 @@
using \<open>S \<noteq> {}\<close> cone_iff[of "convex hull S"] by auto
qed
-subsection \<open>Convex set as intersection of halfspaces\<close>
+subsection%unimportant \<open>Convex set as intersection of halfspaces\<close>
lemma convex_halfspace_intersection:
fixes s :: "('a::euclidean_space) set"
@@ -6381,10 +6381,10 @@
done
qed
-lemma radon:
+theorem%important radon:
assumes "affine_dependent c"
obtains m p where "m \<subseteq> c" "p \<subseteq> c" "m \<inter> p = {}" "(convex hull m) \<inter> (convex hull p) \<noteq> {}"
-proof -
+proof%unimportant -
from assms[unfolded affine_dependent_explicit]
obtain s u where
"finite s" "s \<subseteq> c" "sum u s = 0" "\<exists>v\<in>s. u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0"
@@ -6503,12 +6503,12 @@
qed auto
qed
-lemma helly:
+theorem%important helly:
fixes f :: "'a::euclidean_space set set"
assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
and "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
shows "\<Inter>f \<noteq> {}"
- apply (rule helly_induct)
+ apply%unimportant (rule helly_induct)
using assms
apply auto
done
@@ -6516,7 +6516,7 @@
subsection \<open>Epigraphs of convex functions\<close>
-definition "epigraph s (f :: _ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
+definition%important "epigraph s (f :: _ \<Rightarrow> real) = {xy. fst xy \<in> s \<and> f (fst xy) \<le> snd xy}"
lemma mem_epigraph: "(x, y) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y"
unfolding epigraph_def by auto
@@ -6545,7 +6545,7 @@
by (simp add: convex_epigraph)
-subsubsection \<open>Use this to derive general bound property of convex function\<close>
+subsubsection%unimportant \<open>Use this to derive general bound property of convex function\<close>
lemma convex_on:
assumes "convex s"
@@ -6572,7 +6572,7 @@
done
-subsection \<open>Convexity of general and special intervals\<close>
+subsection%unimportant \<open>Convexity of general and special intervals\<close>
lemma is_interval_convex:
fixes s :: "'a::euclidean_space set"
@@ -6657,7 +6657,7 @@
"\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
using aff_dim_sing connected_imp_perfect by blast
-subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
+subsection%unimportant \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
lemma mem_is_interval_1_I:
fixes a b c::real
@@ -6742,7 +6742,7 @@
by (auto simp: is_interval_convex_1 convex_cball)
-subsection \<open>Another intermediate value theorem formulation\<close>
+subsection%unimportant \<open>Another intermediate value theorem formulation\<close>
lemma ivt_increasing_component_on_1:
fixes f :: "real \<Rightarrow> 'a::euclidean_space"
@@ -6787,7 +6787,7 @@
by (rule ivt_decreasing_component_on_1) (auto simp: continuous_at_imp_continuous_on)
-subsection \<open>A bound within a convex hull, and so an interval\<close>
+subsection%unimportant \<open>A bound within a convex hull, and so an interval\<close>
lemma convex_on_convex_hull_bound:
assumes "convex_on (convex hull s) f"
@@ -6992,7 +6992,7 @@
done
qed
-subsubsection\<open>Representation of any interval as a finite convex hull\<close>
+subsubsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
lemma image_stretch_interval:
"(\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) =
@@ -7069,7 +7069,7 @@
qed
-subsection \<open>Bounded convex function on open set is continuous\<close>
+subsection%unimportant \<open>Bounded convex function on open set is continuous\<close>
lemma convex_on_bounded_continuous:
fixes s :: "('a::real_normed_vector) set"
@@ -7186,7 +7186,7 @@
qed
-subsection \<open>Upper bound on a ball implies upper and lower bounds\<close>
+subsection%unimportant \<open>Upper bound on a ball implies upper and lower bounds\<close>
lemma convex_bounds_lemma:
fixes x :: "'a::real_normed_vector"
@@ -7220,7 +7220,7 @@
qed
-subsubsection \<open>Hence a convex function on an open set is continuous\<close>
+subsubsection%unimportant \<open>Hence a convex function on an open set is continuous\<close>
lemma real_of_nat_ge_one_iff: "1 \<le> real (n::nat) \<longleftrightarrow> 1 \<le> n"
by auto
--- a/src/HOL/Analysis/Euclidean_Space.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Euclidean_Space.thy Fri Apr 06 17:34:50 2018 +0200
@@ -12,7 +12,7 @@
subsection \<open>Type class of Euclidean spaces\<close>
-class euclidean_space = real_inner +
+class%important euclidean_space = real_inner +
fixes Basis :: "'a set"
assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
assumes finite_Basis [simp]: "finite Basis"
@@ -152,7 +152,7 @@
using False by (auto simp: inner_sum_left)
qed
-subsection \<open>Subclass relationships\<close>
+subsection%unimportant \<open>Subclass relationships\<close>
instance euclidean_space \<subseteq> perfect_space
proof
@@ -175,9 +175,9 @@
subsection \<open>Class instances\<close>
-subsubsection \<open>Type @{typ real}\<close>
+subsubsection%unimportant \<open>Type @{typ real}\<close>
-instantiation real :: euclidean_space
+instantiation%important real :: euclidean_space
begin
definition
@@ -191,9 +191,9 @@
lemma DIM_real[simp]: "DIM(real) = 1"
by simp
-subsubsection \<open>Type @{typ complex}\<close>
+subsubsection%unimportant \<open>Type @{typ complex}\<close>
-instantiation complex :: euclidean_space
+instantiation%important complex :: euclidean_space
begin
definition Basis_complex_def: "Basis = {1, \<i>}"
@@ -206,9 +206,9 @@
lemma DIM_complex[simp]: "DIM(complex) = 2"
unfolding Basis_complex_def by simp
-subsubsection \<open>Type @{typ "'a \<times> 'b"}\<close>
+subsubsection%unimportant \<open>Type @{typ "'a \<times> 'b"}\<close>
-instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
+instantiation%important prod :: (euclidean_space, euclidean_space) euclidean_space
begin
definition
--- a/src/HOL/Analysis/Inner_Product.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Inner_Product.thy Fri Apr 06 17:34:50 2018 +0200
@@ -27,7 +27,7 @@
setup \<open>Sign.add_const_constraint
(@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
-class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
+class%important real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
assumes inner_commute: "inner x y = inner y x"
and inner_add_left: "inner (x + y) z = inner x z + inner y z"
@@ -236,7 +236,7 @@
subsection \<open>Class instances\<close>
-instantiation real :: real_inner
+instantiation%important real :: real_inner
begin
definition inner_real_def [simp]: "inner = ( * )"
@@ -265,7 +265,7 @@
and real_inner_1_right[simp]: "inner x 1 = x"
by simp_all
-instantiation complex :: real_inner
+instantiation%important complex :: real_inner
begin
definition inner_complex_def:
@@ -357,7 +357,7 @@
subsection \<open>Gradient derivative\<close>
-definition
+definition%important
gderiv ::
"['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
--- a/src/HOL/Analysis/Linear_Algebra.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Linear_Algebra.thy Fri Apr 06 17:34:50 2018 +0200
@@ -36,7 +36,7 @@
subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
-definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75)
+definition%important hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75)
where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
lemma hull_same: "S s \<Longrightarrow> S hull s = s"
@@ -109,10 +109,10 @@
subsection \<open>Linear functions.\<close>
-lemma linear_iff:
+lemma%important linear_iff:
"linear f \<longleftrightarrow> (\<forall>x y. f (x + y) = f x + f y) \<and> (\<forall>c x. f (c *\<^sub>R x) = c *\<^sub>R f x)"
(is "linear f \<longleftrightarrow> ?rhs")
-proof
+proof%unimportant
assume "linear f"
then interpret f: linear f .
show "?rhs" by (simp add: f.add f.scaleR)
@@ -230,11 +230,11 @@
subsection \<open>Subspaces of vector spaces\<close>
-definition (in real_vector) subspace :: "'a set \<Rightarrow> bool"
+definition%important (in real_vector) subspace :: "'a set \<Rightarrow> bool"
where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x \<in> S. \<forall>y \<in> S. x + y \<in> S) \<and> (\<forall>c. \<forall>x \<in> S. c *\<^sub>R x \<in> S)"
-definition (in real_vector) "span S = (subspace hull S)"
-definition (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
+definition%important (in real_vector) "span S = (subspace hull S)"
+definition%important (in real_vector) "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span (S - {a}))"
abbreviation (in real_vector) "independent s \<equiv> \<not> dependent s"
text \<open>Closure properties of subspaces.\<close>
@@ -284,7 +284,7 @@
apply (metis add.assoc add.left_commute)
using scaleR_add_right by blast
-subsection \<open>Properties of span\<close>
+subsection%unimportant \<open>Properties of span\<close>
lemma (in real_vector) span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
by (metis span_def hull_mono)
@@ -1351,7 +1351,7 @@
qed
-subsection \<open>More interesting properties of the norm.\<close>
+subsection%unimportant \<open>More interesting properties of the norm.\<close>
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
by auto
@@ -1498,11 +1498,11 @@
subsection \<open>Orthogonality.\<close>
+definition%important (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
+
context real_inner
begin
-definition "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
-
lemma orthogonal_self: "orthogonal x x \<longleftrightarrow> x = 0"
by (simp add: orthogonal_def)
@@ -1567,7 +1567,7 @@
subsection \<open>Bilinear functions.\<close>
-definition "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
+definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
by (simp add: bilinear_def linear_iff)
@@ -1630,7 +1630,7 @@
subsection \<open>Adjoints.\<close>
-definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
+definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
lemma adjoint_unique:
assumes "\<forall>x y. inner (f x) y = inner x (g y)"
@@ -1701,7 +1701,7 @@
by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])
-subsection \<open>Interlude: Some properties of real sets\<close>
+subsection%unimportant \<open>Interlude: Some properties of real sets\<close>
lemma seq_mono_lemma:
assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n"
@@ -1754,11 +1754,11 @@
subsection \<open>Archimedean properties and useful consequences\<close>
text\<open>Bernoulli's inequality\<close>
-proposition Bernoulli_inequality:
+proposition%important Bernoulli_inequality:
fixes x :: real
assumes "-1 \<le> x"
shows "1 + n * x \<le> (1 + x) ^ n"
-proof (induct n)
+proof%unimportant (induct n)
case 0
then show ?case by simp
next
@@ -1844,7 +1844,7 @@
done
-subsection \<open>Euclidean Spaces as Typeclass\<close>
+subsection%unimportant \<open>Euclidean Spaces as Typeclass\<close>
lemma independent_Basis: "independent Basis"
unfolding dependent_def
@@ -1905,7 +1905,7 @@
qed
-subsection \<open>Linearity and Bilinearity continued\<close>
+subsection%unimportant \<open>Linearity and Bilinearity continued\<close>
lemma linear_bounded:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -2074,7 +2074,7 @@
by (metis linear_imp_has_derivative differentiable_def)
-subsection \<open>We continue.\<close>
+subsection%unimportant \<open>We continue.\<close>
lemma independent_bound:
fixes S :: "'a::euclidean_space set"
@@ -2879,7 +2879,7 @@
subsection \<open>Infinity norm\<close>
-definition "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
+definition%important "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
lemma infnorm_set_image:
fixes x :: "'a::euclidean_space"
@@ -3115,7 +3115,7 @@
subsection \<open>Collinearity\<close>
-definition collinear :: "'a::real_vector set \<Rightarrow> bool"
+definition%important collinear :: "'a::real_vector set \<Rightarrow> bool"
where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
lemma collinear_alt:
--- a/src/HOL/Analysis/Measurable.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Measurable.thy Fri Apr 06 17:34:50 2018 +0200
@@ -1,13 +1,13 @@
(* Title: HOL/Analysis/Measurable.thy
Author: Johannes Hölzl <hoelzl@in.tum.de>
*)
+section \<open>Measurability prover\<close>
theory Measurable
imports
Sigma_Algebra
"HOL-Library.Order_Continuity"
begin
-subsection \<open>Measurability prover\<close>
lemma (in algebra) sets_Collect_finite_All:
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S"
@@ -64,10 +64,10 @@
attribute_setup measurable_cong = Measurable.cong_thm_attr
"add congurence rules to measurability prover"
-method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
+method_setup%important measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
"measurability prover"
-simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = \<open>K Measurable.simproc\<close>
+simproc_setup%important measurable ("A \<in> sets M" | "f \<in> measurable M N") = \<open>K Measurable.simproc\<close>
setup \<open>
Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all)
@@ -380,7 +380,7 @@
unfolding pred_def
by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)
-subsection \<open>Measurability for (co)inductive predicates\<close>
+subsection%unimportant \<open>Measurability for (co)inductive predicates\<close>
lemma measurable_bot[measurable]: "bot \<in> measurable M (count_space UNIV)"
by (simp add: bot_fun_def)
--- a/src/HOL/Analysis/Measure_Space.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Measure_Space.thy Fri Apr 06 17:34:50 2018 +0200
@@ -11,7 +11,7 @@
Measurable "HOL-Library.Extended_Nonnegative_Real"
begin
-subsection "Relate extended reals and the indicator function"
+subsection%unimportant "Relate extended reals and the indicator function"
lemma suminf_cmult_indicator:
fixes f :: "nat \<Rightarrow> ennreal"
@@ -59,7 +59,7 @@
represent sigma algebras (with an arbitrary emeasure).
\<close>
-subsection "Extend binary sets"
+subsection%unimportant "Extend binary sets"
lemma LIMSEQ_binaryset:
assumes f: "f {} = 0"
@@ -91,7 +91,7 @@
shows "f {} = 0 \<Longrightarrow> (\<Sum>n. f (binaryset A B n)) = f A + f B"
by (metis binaryset_sums sums_unique)
-subsection \<open>Properties of a premeasure @{term \<mu>}\<close>
+subsection%unimportant \<open>Properties of a premeasure @{term \<mu>}\<close>
text \<open>
The definitions for @{const positive} and @{const countably_additive} should be here, by they are
@@ -442,7 +442,7 @@
using empty_continuous_imp_continuous_from_below[OF f fin] cont
by blast
-subsection \<open>Properties of @{const emeasure}\<close>
+subsection%unimportant \<open>Properties of @{const emeasure}\<close>
lemma emeasure_positive: "positive (sets M) (emeasure M)"
by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
@@ -881,7 +881,7 @@
subsection \<open>\<open>\<mu>\<close>-null sets\<close>
-definition null_sets :: "'a measure \<Rightarrow> 'a set set" where
+definition%important null_sets :: "'a measure \<Rightarrow> 'a set set" where
"null_sets M = {N\<in>sets M. emeasure M N = 0}"
lemma null_setsD1[dest]: "A \<in> null_sets M \<Longrightarrow> emeasure M A = 0"
@@ -989,7 +989,7 @@
subsection \<open>The almost everywhere filter (i.e.\ quantifier)\<close>
-definition ae_filter :: "'a measure \<Rightarrow> 'a filter" where
+definition%important ae_filter :: "'a measure \<Rightarrow> 'a filter" where
"ae_filter M = (INF N:null_sets M. principal (space M - N))"
abbreviation almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
@@ -1265,7 +1265,7 @@
subsection \<open>\<open>\<sigma>\<close>-finite Measures\<close>
-locale sigma_finite_measure =
+locale%important sigma_finite_measure =
fixes M :: "'a measure"
assumes sigma_finite_countable:
"\<exists>A::'a set set. countable A \<and> A \<subseteq> sets M \<and> (\<Union>A) = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)"
@@ -1387,7 +1387,7 @@
subsection \<open>Measure space induced by distribution of @{const measurable}-functions\<close>
-definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
+definition%important distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
"distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
lemma
@@ -1513,12 +1513,12 @@
"f \<in> measurable M N \<Longrightarrow> A \<in> null_sets (distr M N f) \<longleftrightarrow> f -` A \<inter> space M \<in> null_sets M \<and> A \<in> sets N"
by (auto simp add: null_sets_def emeasure_distr)
-lemma distr_distr:
+lemma%important distr_distr:
"g \<in> measurable N L \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> distr (distr M N f) L g = distr M L (g \<circ> f)"
by (auto simp add: emeasure_distr measurable_space
intro!: arg_cong[where f="emeasure M"] measure_eqI)
-subsection \<open>Real measure values\<close>
+subsection%unimportant \<open>Real measure values\<close>
lemma ring_of_finite_sets: "ring_of_sets (space M) {A\<in>sets M. emeasure M A \<noteq> top}"
proof (rule ring_of_setsI)
@@ -1705,7 +1705,7 @@
subsection \<open>Set of measurable sets with finite measure\<close>
-definition fmeasurable :: "'a measure \<Rightarrow> 'a set set"
+definition%important fmeasurable :: "'a measure \<Rightarrow> 'a set set"
where
"fmeasurable M = {A\<in>sets M. emeasure M A < \<infinity>}"
@@ -1972,7 +1972,7 @@
subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
-locale finite_measure = sigma_finite_measure M for M +
+locale%important finite_measure = sigma_finite_measure M for M +
assumes finite_emeasure_space: "emeasure M (space M) \<noteq> top"
lemma finite_measureI[Pure.intro!]:
@@ -2194,7 +2194,7 @@
using bound[of x] sets_eq_imp_space_eq[OF sets] by (simp add: iter)
qed (auto simp add: iter le_fun_def INF_apply[abs_def] intro!: meas cont)
-subsection \<open>Counting space\<close>
+subsection%unimportant \<open>Counting space\<close>
lemma strict_monoI_Suc:
assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
@@ -2343,7 +2343,7 @@
show "sigma_finite_measure (count_space A)" ..
qed
-subsection \<open>Measure restricted to space\<close>
+subsection%unimportant \<open>Measure restricted to space\<close>
lemma emeasure_restrict_space:
assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
@@ -2502,7 +2502,7 @@
finally show "emeasure M X = emeasure N X" .
qed fact
-subsection \<open>Null measure\<close>
+subsection%unimportant \<open>Null measure\<close>
definition "null_measure M = sigma (space M) (sets M)"
@@ -2525,7 +2525,7 @@
subsection \<open>Scaling a measure\<close>
-definition scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+definition%important scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
where
"scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. r * emeasure M A)"
@@ -2703,11 +2703,11 @@
qed auto
qed
-lemma unsigned_Hahn_decomposition:
+lemma%important unsigned_Hahn_decomposition:
assumes [simp]: "sets N = sets M" and [measurable]: "A \<in> sets M"
and [simp]: "emeasure M A \<noteq> top" "emeasure N A \<noteq> top"
shows "\<exists>Y\<in>sets M. Y \<subseteq> A \<and> (\<forall>X\<in>sets M. X \<subseteq> Y \<longrightarrow> N X \<le> M X) \<and> (\<forall>X\<in>sets M. X \<subseteq> A \<longrightarrow> X \<inter> Y = {} \<longrightarrow> M X \<le> N X)"
-proof -
+proof%unimportant -
have "\<exists>Y\<in>sets (restrict_space M A).
(\<forall>X\<in>sets (restrict_space M A). X \<subseteq> Y \<longrightarrow> (restrict_space N A) X \<le> (restrict_space M A) X) \<and>
(\<forall>X\<in>sets (restrict_space M A). X \<inter> Y = {} \<longrightarrow> (restrict_space M A) X \<le> (restrict_space N A) X)"
@@ -2728,12 +2728,12 @@
done
qed
-text \<open>
+text%important \<open>
Define a lexicographical order on @{type measure}, in the order space, sets and measure. The parts
of the lexicographical order are point-wise ordered.
\<close>
-instantiation measure :: (type) order_bot
+instantiation%important measure :: (type) order_bot
begin
inductive less_eq_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
@@ -2746,10 +2746,10 @@
if sets M = sets N then emeasure M \<le> emeasure N else sets M \<subseteq> sets N else space M \<subseteq> space N)"
by (auto elim: less_eq_measure.cases intro: less_eq_measure.intros)
-definition less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
+definition%important less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
"less_measure M N \<longleftrightarrow> (M \<le> N \<and> \<not> N \<le> M)"
-definition bot_measure :: "'a measure" where
+definition%important bot_measure :: "'a measure" where
"bot_measure = sigma {} {}"
lemma
@@ -2766,13 +2766,14 @@
end
-lemma le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
+lemma%important le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
+ apply%unimportant -
apply (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq)
subgoal for X
by (cases "X \<in> sets M") (auto simp: emeasure_notin_sets)
done
-definition sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+definition%important sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
where
"sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
@@ -2900,7 +2901,7 @@
qed
qed simp_all
-definition sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+definition%important sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
where
"sup_lexord A B k s c =
(if k A = k B then c else if \<not> k A \<le> k B \<and> \<not> k B \<le> k A then s else if k B \<le> k A then A else B)"
@@ -2926,10 +2927,10 @@
(simp_all add: eq_commute[of _ "sets x"] le_measure_iff emeasure_sigma le_fun_def
sigma_sets_superset_generator sigma_sets_le_sets_iff)
-instantiation measure :: (type) semilattice_sup
+instantiation%important measure :: (type) semilattice_sup
begin
-definition sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+definition%important sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
where
"sup_measure A B =
sup_lexord A B space (sigma (space A \<union> space B) {})
@@ -3057,7 +3058,7 @@
by (simp add: A(3))
qed
-instantiation measure :: (type) complete_lattice
+instantiation%important measure :: (type) complete_lattice
begin
interpretation sup_measure: comm_monoid_set sup "bot :: 'a measure"
@@ -3092,7 +3093,7 @@
"finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> sets i = sets M) \<Longrightarrow> sets (sup_measure.F id I) = sets M"
by (induction I rule: finite_ne_induct) (simp_all add: sets_sup)
-definition Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
+definition%important Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
where
"Sup_measure' M = measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
(\<lambda>X. (SUP P:{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
@@ -3163,20 +3164,20 @@
using assms * by auto
qed (rule UN_space_closed)
-definition Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
+definition%important Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
where
"Sup_measure = Sup_lexord space (Sup_lexord sets Sup_measure'
(\<lambda>U. sigma (\<Union>u\<in>U. space u) (\<Union>u\<in>U. sets u))) (\<lambda>U. sigma (\<Union>u\<in>U. space u) {})"
-definition Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
+definition%important Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
where
"Inf_measure A = Sup {x. \<forall>a\<in>A. x \<le> a}"
-definition inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+definition%important inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
where
"inf_measure a b = Inf {a, b}"
-definition top_measure :: "'a measure"
+definition%important top_measure :: "'a measure"
where
"top_measure = Inf {}"
@@ -3417,7 +3418,7 @@
qed
qed
-subsubsection \<open>Supremum of a set of $\sigma$-algebras\<close>
+subsubsection%unimportant \<open>Supremum of a set of $\sigma$-algebras\<close>
lemma space_Sup_eq_UN: "space (Sup M) = (\<Union>x\<in>M. space x)"
unfolding Sup_measure_def
--- a/src/HOL/Analysis/Norm_Arith.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Norm_Arith.thy Fri Apr 06 17:34:50 2018 +0200
@@ -131,14 +131,14 @@
ML_file "normarith.ML"
-method_setup norm = \<open>
+method_setup%important norm = \<open>
Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
\<close> "prove simple linear statements about vector norms"
text \<open>Hence more metric properties.\<close>
-lemma dist_triangle_add:
+lemma%important dist_triangle_add:
fixes x y x' y' :: "'a::real_normed_vector"
shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
by norm
--- a/src/HOL/Analysis/Path_Connected.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy Fri Apr 06 17:34:50 2018 +0200
@@ -10,34 +10,34 @@
subsection \<open>Paths and Arcs\<close>
-definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
+definition%important path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
where "path g \<longleftrightarrow> continuous_on {0..1} g"
-definition pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
+definition%important pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
where "pathstart g = g 0"
-definition pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
+definition%important pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
where "pathfinish g = g 1"
-definition path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
+definition%important path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
where "path_image g = g ` {0 .. 1}"
-definition reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
+definition%important reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
where "reversepath g = (\<lambda>x. g(1 - x))"
-definition joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a"
+definition%important joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a"
(infixr "+++" 75)
where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x - 1))"
-definition simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
+definition%important simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
where "simple_path g \<longleftrightarrow>
path g \<and> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)"
-definition arc :: "(real \<Rightarrow> 'a :: topological_space) \<Rightarrow> bool"
+definition%important arc :: "(real \<Rightarrow> 'a :: topological_space) \<Rightarrow> bool"
where "arc g \<longleftrightarrow> path g \<and> inj_on g {0..1}"
-subsection\<open>Invariance theorems\<close>
+subsection%unimportant\<open>Invariance theorems\<close>
lemma path_eq: "path p \<Longrightarrow> (\<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t) \<Longrightarrow> path q"
using continuous_on_eq path_def by blast
@@ -132,7 +132,7 @@
using assms inj_on_eq_iff [of f]
by (auto simp: arc_def inj_on_def path_linear_image_eq)
-subsection\<open>Basic lemmas about paths\<close>
+subsection%unimportant\<open>Basic lemmas about paths\<close>
lemma continuous_on_path: "path f \<Longrightarrow> t \<subseteq> {0..1} \<Longrightarrow> continuous_on t f"
using continuous_on_subset path_def by blast
@@ -301,7 +301,7 @@
done
qed
-section \<open>Path Images\<close>
+section%unimportant \<open>Path Images\<close>
lemma bounded_path_image: "path g \<Longrightarrow> bounded(path_image g)"
by (simp add: compact_imp_bounded compact_path_image)
@@ -394,7 +394,7 @@
by (auto simp: simple_path_def path_image_def inj_on_def less_eq_real_def Ball_def)
-subsection\<open>Simple paths with the endpoints removed\<close>
+subsection%unimportant\<open>Simple paths with the endpoints removed\<close>
lemma simple_path_endless:
"simple_path c \<Longrightarrow> path_image c - {pathstart c,pathfinish c} = c ` {0<..<1}"
@@ -417,7 +417,7 @@
by (simp add: simple_path_endless)
-subsection\<open>The operations on paths\<close>
+subsection%unimportant\<open>The operations on paths\<close>
lemma path_image_subset_reversepath: "path_image(reversepath g) \<le> path_image g"
by (auto simp: path_image_def reversepath_def)
@@ -565,7 +565,7 @@
by (rule ext) (auto simp: mult.commute)
-subsection\<open>Some reversed and "if and only if" versions of joining theorems\<close>
+subsection%unimportant\<open>Some reversed and "if and only if" versions of joining theorems\<close>
lemma path_join_path_ends:
fixes g1 :: "real \<Rightarrow> 'a::metric_space"
@@ -698,7 +698,7 @@
using pathfinish_in_path_image by (fastforce simp: arc_join_eq)
-subsection\<open>The joining of paths is associative\<close>
+subsection%unimportant\<open>The joining of paths is associative\<close>
lemma path_assoc:
"\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
@@ -748,7 +748,7 @@
\<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
by (simp add: arc_simple_path simple_path_assoc)
-subsubsection\<open>Symmetry and loops\<close>
+subsubsection%unimportant\<open>Symmetry and loops\<close>
lemma path_sym:
"\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> path(p +++ q) \<longleftrightarrow> path(q +++ p)"
@@ -767,7 +767,7 @@
section\<open>Choosing a subpath of an existing path\<close>
-definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
+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)"
lemma path_image_subpath_gen:
@@ -945,7 +945,7 @@
lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
-subsection\<open>There is a subpath to the frontier\<close>
+subsection%unimportant\<open>There is a subpath to the frontier\<close>
lemma subpath_to_frontier_explicit:
fixes S :: "'a::metric_space set"
@@ -1063,7 +1063,7 @@
subsection \<open>shiftpath: Reparametrizing a closed curve to start at some chosen point\<close>
-definition shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
+definition%important shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
where "shiftpath a f = (\<lambda>x. if (a + x) \<le> 1 then f (a + x) else f (a + x - 1))"
lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart (shiftpath a g) = g a"
@@ -1179,7 +1179,7 @@
subsection \<open>Special case of straight-line paths\<close>
-definition linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a"
+definition%important linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a"
where "linepath a b = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b)"
lemma pathstart_linepath[simp]: "pathstart (linepath a b) = a"
@@ -1259,7 +1259,7 @@
qed
-subsection\<open>Segments via convex hulls\<close>
+subsection%unimportant\<open>Segments via convex hulls\<close>
lemma segments_subset_convex_hull:
"closed_segment a b \<subseteq> (convex hull {a,b,c})"
@@ -1379,7 +1379,7 @@
by (force simp: inj_on_def)
qed
-subsection \<open>Bounding a point away from a path\<close>
+subsection%unimportant \<open>Bounding a point away from a path\<close>
lemma not_on_path_ball:
fixes g :: "real \<Rightarrow> 'a::heine_borel"
@@ -1416,10 +1416,10 @@
section \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close>
-definition "path_component s x y \<longleftrightarrow>
+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
+abbreviation%important
"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
@@ -1471,7 +1471,7 @@
done
-subsubsection \<open>Path components as sets\<close>
+subsubsection%unimportant \<open>Path components as sets\<close>
lemma path_component_set:
"path_component_set s x =
@@ -1495,7 +1495,7 @@
subsection \<open>Path connectedness of a space\<close>
-definition "path_connected s \<longleftrightarrow>
+definition%important "path_connected s \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>y\<in>s. \<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"
lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
@@ -1806,7 +1806,7 @@
using path_component_eq_empty by auto
qed
-subsection\<open>Lemmas about path-connectedness\<close>
+subsection%unimportant\<open>Lemmas about path-connectedness\<close>
lemma path_connected_linear_image:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
@@ -1878,7 +1878,7 @@
using is_interval_connected_1 is_interval_path_connected path_connected_imp_connected by blast
-subsection\<open>Path components\<close>
+subsection%unimportant\<open>Path components\<close>
lemma Union_path_component [simp]:
"Union {path_component_set S x |x. x \<in> S} = S"
@@ -1990,11 +1990,11 @@
"2 \<le> DIM('N::euclidean_space) \<Longrightarrow> connected(- {a::'N})"
by (simp add: path_connected_punctured_universe path_connected_imp_connected)
-lemma path_connected_sphere:
+lemma%important path_connected_sphere:
fixes a :: "'a :: euclidean_space"
assumes "2 \<le> DIM('a)"
shows "path_connected(sphere a r)"
-proof (cases r "0::real" rule: linorder_cases)
+proof%unimportant (cases r "0::real" rule: linorder_cases)
case less
then show ?thesis
by (simp add: path_connected_empty)
@@ -2315,26 +2315,26 @@
using path_connected_translation by metis
qed
-lemma path_connected_annulus:
+lemma%important path_connected_annulus:
fixes a :: "'N::euclidean_space"
assumes "2 \<le> DIM('N)"
shows "path_connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
"path_connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
"path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
"path_connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
- by (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
-
-lemma connected_annulus:
+ by%unimportant (auto simp: is_interval_def intro!: is_interval_convex convex_imp_path_connected path_connected_2DIM_I [OF assms])
+
+lemma%important connected_annulus:
fixes a :: "'N::euclidean_space"
assumes "2 \<le> DIM('N::euclidean_space)"
shows "connected {x. r1 < norm(x - a) \<and> norm(x - a) < r2}"
"connected {x. r1 < norm(x - a) \<and> norm(x - a) \<le> r2}"
"connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) < r2}"
"connected {x. r1 \<le> norm(x - a) \<and> norm(x - a) \<le> r2}"
- by (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
-
-
-subsection\<open>Relations between components and path components\<close>
+ by%unimportant (auto simp: path_connected_annulus [OF assms] path_connected_imp_connected)
+
+
+subsection%unimportant\<open>Relations between components and path components\<close>
lemma open_connected_component:
fixes s :: "'a::real_normed_vector set"
@@ -2439,7 +2439,7 @@
qed
-subsection\<open>Existence of unbounded components\<close>
+subsection%unimportant\<open>Existence of unbounded components\<close>
lemma cobounded_unbounded_component:
fixes s :: "'a :: euclidean_space set"
@@ -2527,13 +2527,13 @@
section\<open>The "inside" and "outside" of a set\<close>
-text\<open>The inside comprises the points in a bounded connected component of the set's complement.
+text%important\<open>The inside comprises the points in a bounded connected component of the set's complement.
The outside comprises the points in unbounded connected component of the complement.\<close>
-definition inside where
+definition%important inside where
"inside s \<equiv> {x. (x \<notin> s) \<and> bounded(connected_component_set ( - s) x)}"
-definition outside where
+definition%important outside where
"outside s \<equiv> -s \<inter> {x. ~ bounded(connected_component_set (- s) x)}"
lemma outside: "outside s = {x. ~ bounded(connected_component_set (- s) x)}"
@@ -3329,14 +3329,14 @@
subsection\<open>Condition for an open map's image to contain a ball\<close>
-lemma ball_subset_open_map_image:
+lemma%important ball_subset_open_map_image:
fixes f :: "'a::heine_borel \<Rightarrow> 'b :: {real_normed_vector,heine_borel}"
assumes contf: "continuous_on (closure S) f"
and oint: "open (f ` interior S)"
and le_no: "\<And>z. z \<in> frontier S \<Longrightarrow> r \<le> norm(f z - f a)"
and "bounded S" "a \<in> S" "0 < r"
shows "ball (f a) r \<subseteq> f ` S"
-proof (cases "f ` S = UNIV")
+proof%unimportant (cases "f ` S = UNIV")
case True then show ?thesis by simp
next
case False
@@ -3382,10 +3382,10 @@
section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps.\<close>
-text\<open> We often just want to require that it fixes some subset, but to take in
+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>
-definition homotopic_with ::
+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"
where
"homotopic_with P X Y p q \<equiv>
@@ -3487,7 +3487,7 @@
qed
-subsection\<open> Trivial properties.\<close>
+subsection%unimportant\<open> Trivial properties.\<close>
lemma homotopic_with_imp_property: "homotopic_with P X Y f g \<Longrightarrow> P f \<and> P g"
unfolding homotopic_with_def Ball_def
@@ -3745,7 +3745,7 @@
subsection\<open>Homotopy of paths, maintaining the same endpoints.\<close>
-definition homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
+definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
where
"homotopic_paths s p q \<equiv>
homotopic_with (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
@@ -3897,28 +3897,28 @@
subsection\<open>Group properties for homotopy of paths\<close>
-text\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
-
-proposition homotopic_paths_rid:
+text%important\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
+
+proposition%important homotopic_paths_rid:
"\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (p +++ linepath (pathfinish p) (pathfinish p)) p"
- apply (subst homotopic_paths_sym)
+ apply%unimportant (subst homotopic_paths_sym)
apply (rule homotopic_paths_reparametrize [where f = "\<lambda>t. if t \<le> 1 / 2 then 2 *\<^sub>R t else 1"])
apply (simp_all del: le_divide_eq_numeral1)
apply (subst split_01)
apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
done
-proposition homotopic_paths_lid:
+proposition%important homotopic_paths_lid:
"\<lbrakk>path p; path_image p \<subseteq> s\<rbrakk> \<Longrightarrow> homotopic_paths s (linepath (pathstart p) (pathstart p) +++ p) p"
-using homotopic_paths_rid [of "reversepath p" s]
+using%unimportant homotopic_paths_rid [of "reversepath p" s]
by (metis homotopic_paths_reversepath path_image_reversepath path_reversepath pathfinish_linepath
pathfinish_reversepath reversepath_joinpaths reversepath_linepath)
-proposition homotopic_paths_assoc:
+proposition%important homotopic_paths_assoc:
"\<lbrakk>path p; path_image p \<subseteq> s; path q; path_image q \<subseteq> s; path r; path_image r \<subseteq> s; pathfinish p = pathstart q;
pathfinish q = pathstart r\<rbrakk>
\<Longrightarrow> homotopic_paths s (p +++ (q +++ r)) ((p +++ q) +++ r)"
- apply (subst homotopic_paths_sym)
+ apply%unimportant (subst homotopic_paths_sym)
apply (rule homotopic_paths_reparametrize
[where f = "\<lambda>t. if t \<le> 1 / 2 then inverse 2 *\<^sub>R t
else if t \<le> 3 / 4 then t - (1 / 4)
@@ -3929,10 +3929,10 @@
apply (auto simp: joinpaths_def)
done
-proposition homotopic_paths_rinv:
+proposition%important homotopic_paths_rinv:
assumes "path p" "path_image p \<subseteq> s"
shows "homotopic_paths s (p +++ reversepath p) (linepath (pathstart p) (pathstart p))"
-proof -
+proof%unimportant -
have "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. (subpath 0 (fst x) p +++ reversepath (subpath 0 (fst x) p)) (snd x))"
using assms
apply (simp add: joinpaths_def subpath_def reversepath_def path_def del: le_divide_eq_numeral1)
@@ -3952,15 +3952,15 @@
done
qed
-proposition homotopic_paths_linv:
+proposition%important homotopic_paths_linv:
assumes "path p" "path_image p \<subseteq> s"
shows "homotopic_paths s (reversepath p +++ p) (linepath (pathfinish p) (pathfinish p))"
-using homotopic_paths_rinv [of "reversepath p" s] assms by simp
+using%unimportant homotopic_paths_rinv [of "reversepath p" s] assms by simp
subsection\<open> Homotopy of loops without requiring preservation of endpoints.\<close>
-definition homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool" where
+definition%important homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool" where
"homotopic_loops s p q \<equiv>
homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
@@ -4025,14 +4025,14 @@
subsection\<open>Relations between the two variants of homotopy\<close>
-proposition homotopic_paths_imp_homotopic_loops:
+proposition%important homotopic_paths_imp_homotopic_loops:
"\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
- by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
-
-proposition homotopic_loops_imp_homotopic_paths_null:
+ by%unimportant (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
+
+proposition%important homotopic_loops_imp_homotopic_paths_null:
assumes "homotopic_loops s p (linepath a a)"
shows "homotopic_paths s p (linepath (pathstart p) (pathstart p))"
-proof -
+proof%unimportant -
have "path p" by (metis assms homotopic_loops_imp_path)
have ploop: "pathfinish p = pathstart p" by (metis assms homotopic_loops_imp_loop)
have pip: "path_image p \<subseteq> s" by (metis assms homotopic_loops_imp_subset)
@@ -4100,12 +4100,12 @@
by (blast intro: homotopic_paths_trans)
qed
-proposition homotopic_loops_conjugate:
+proposition%important homotopic_loops_conjugate:
fixes s :: "'a::real_normed_vector set"
assumes "path p" "path q" and pip: "path_image p \<subseteq> s" and piq: "path_image q \<subseteq> s"
and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
shows "homotopic_loops s (p +++ q +++ reversepath p) q"
-proof -
+proof%unimportant -
have contp: "continuous_on {0..1} p" using \<open>path p\<close> [unfolded path_def] by blast
have contq: "continuous_on {0..1} q" using \<open>path q\<close> [unfolded path_def] by blast
have c1: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>x. p ((1 - fst x) * snd x + fst x))"
@@ -4197,7 +4197,7 @@
qed
-subsection\<open> Homotopy of "nearby" function, paths and loops.\<close>
+subsection%unimportant\<open> Homotopy of "nearby" function, paths and loops.\<close>
lemma homotopic_with_linear:
fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
@@ -4358,10 +4358,10 @@
using homotopic_join_subpaths2 by blast
qed
-proposition homotopic_join_subpaths:
+proposition%important homotopic_join_subpaths:
"\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
\<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
-apply (rule le_cases3 [of u v w])
+apply%unimportant (rule le_cases3 [of u v w])
using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
@@ -4399,9 +4399,9 @@
subsection\<open>Simply connected sets\<close>
-text\<open>defined as "all loops are homotopic (as loops)\<close>
-
-definition simply_connected where
+text%important\<open>defined as "all loops are homotopic (as loops)\<close>
+
+definition%important simply_connected where
"simply_connected S \<equiv>
\<forall>p q. path p \<and> pathfinish p = pathstart p \<and> path_image p \<subseteq> S \<and>
path q \<and> pathfinish q = pathstart q \<and> path_image q \<subseteq> S
@@ -4583,7 +4583,7 @@
subsection\<open>Contractible sets\<close>
-definition contractible where
+definition%important contractible where
"contractible S \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
proposition contractible_imp_simply_connected:
@@ -4846,7 +4846,7 @@
subsection\<open>Local versions of topological properties in general\<close>
-definition locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+definition%important locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
where
"locally P S \<equiv>
\<forall>w x. openin (subtopology euclidean S) w \<and> x \<in> w
@@ -5077,7 +5077,7 @@
subsection\<open>Sort of induction principle for connected sets\<close>
-lemma connected_induction:
+lemma%important connected_induction:
assumes "connected S"
and opD: "\<And>T a. \<lbrakk>openin (subtopology euclidean S) T; a \<in> T\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> T \<and> P z"
and opI: "\<And>a. a \<in> S
@@ -5085,7 +5085,7 @@
(\<forall>x \<in> T. \<forall>y \<in> T. P x \<and> P y \<and> Q x \<longrightarrow> Q y)"
and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
shows "Q b"
-proof -
+proof%unimportant -
have 1: "openin (subtopology euclidean S)
{b. \<exists>T. openin (subtopology euclidean S) T \<and>
b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
@@ -5176,14 +5176,14 @@
subsection\<open>Basic properties of local compactness\<close>
-lemma locally_compact:
+lemma%important locally_compact:
fixes s :: "'a :: metric_space set"
shows
"locally compact s \<longleftrightarrow>
(\<forall>x \<in> s. \<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
openin (subtopology euclidean s) u \<and> compact v)"
(is "?lhs = ?rhs")
-proof
+proof%unimportant
assume ?lhs
then show ?rhs
apply clarify
@@ -5730,12 +5730,12 @@
by (metis \<open>U = S \<inter> V\<close> inf.bounded_iff openin_imp_subset that)
qed
-corollary Sura_Bura:
+corollary%important Sura_Bura:
fixes S :: "'a::euclidean_space set"
assumes "locally compact S" "C \<in> components S" "compact C"
shows "C = \<Inter> {K. C \<subseteq> K \<and> compact K \<and> openin (subtopology euclidean S) K}"
(is "C = ?rhs")
-proof
+proof%unimportant
show "?rhs \<subseteq> C"
proof (clarsimp, rule ccontr)
fix x
@@ -5865,17 +5865,17 @@
by (metis assms(1) assms(2) assms(3) mem_Collect_eq path_component_subset path_connected_path_component)
qed
-proposition locally_path_connected:
+proposition%important locally_path_connected:
"locally path_connected S \<longleftrightarrow>
(\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
\<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))"
-by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
-
-proposition locally_path_connected_open_path_component:
+by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
+
+proposition%important locally_path_connected_open_path_component:
"locally path_connected S \<longleftrightarrow>
(\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
\<longrightarrow> openin (subtopology euclidean S) (path_component_set t x))"
-by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
+by%unimportant (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
lemma locally_connected_open_component:
"locally connected S \<longleftrightarrow>
@@ -5883,14 +5883,14 @@
\<longrightarrow> openin (subtopology euclidean S) c)"
by (metis components_iff locally_connected_open_connected_component)
-proposition locally_connected_im_kleinen:
+proposition%important locally_connected_im_kleinen:
"locally connected S \<longleftrightarrow>
(\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
\<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
x \<in> u \<and> u \<subseteq> v \<and>
(\<forall>y. y \<in> u \<longrightarrow> (\<exists>c. connected c \<and> c \<subseteq> v \<and> x \<in> c \<and> y \<in> c))))"
(is "?lhs = ?rhs")
-proof
+proof%unimportant
assume ?lhs
then show ?rhs
by (fastforce simp add: locally_connected)
@@ -5924,7 +5924,7 @@
done
qed
-proposition locally_path_connected_im_kleinen:
+proposition%important locally_path_connected_im_kleinen:
"locally path_connected S \<longleftrightarrow>
(\<forall>v x. openin (subtopology euclidean S) v \<and> x \<in> v
\<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and>
@@ -5932,7 +5932,7 @@
(\<forall>y. y \<in> u \<longrightarrow> (\<exists>p. path p \<and> path_image p \<subseteq> v \<and>
pathstart p = x \<and> pathfinish p = y))))"
(is "?lhs = ?rhs")
-proof
+proof%unimportant
assume ?lhs
then show ?rhs
apply (simp add: locally_path_connected path_connected_def)
@@ -6082,13 +6082,13 @@
shows "open S \<Longrightarrow> path_component_set S x = connected_component_set S x"
by (simp add: open_path_connected_component)
-proposition locally_connected_quotient_image:
+proposition%important locally_connected_quotient_image:
assumes lcS: "locally connected S"
and oo: "\<And>T. T \<subseteq> f ` S
\<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow>
openin (subtopology euclidean (f ` S)) T"
shows "locally connected (f ` S)"
-proof (clarsimp simp: locally_connected_open_component)
+proof%unimportant (clarsimp simp: locally_connected_open_component)
fix U C
assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "C \<in> components U"
then have "C \<subseteq> U" "U \<subseteq> f ` S"
@@ -6148,12 +6148,12 @@
qed
text\<open>The proof resembles that above but is not identical!\<close>
-proposition locally_path_connected_quotient_image:
+proposition%important locally_path_connected_quotient_image:
assumes lcS: "locally path_connected S"
and oo: "\<And>T. T \<subseteq> f ` S
\<Longrightarrow> openin (subtopology euclidean S) (S \<inter> f -` T) \<longleftrightarrow> openin (subtopology euclidean (f ` S)) T"
shows "locally path_connected (f ` S)"
-proof (clarsimp simp: locally_path_connected_open_path_component)
+proof%unimportant (clarsimp simp: locally_path_connected_open_path_component)
fix U y
assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "y \<in> U"
then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
@@ -6221,7 +6221,7 @@
by metis
qed
-subsection\<open>Components, continuity, openin, closedin\<close>
+subsection%unimportant\<open>Components, continuity, openin, closedin\<close>
lemma continuous_on_components_gen:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
@@ -6324,7 +6324,8 @@
fixes S :: "'a::real_normed_vector set"
assumes S: "closed S" and c: " c \<in> components(-S)"
shows "closed (S \<union> c)"
-by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component locally_connected_UNIV subtopology_UNIV)
+ by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component
+ locally_connected_UNIV subtopology_UNIV)
subsection\<open>Existence of isometry between subspaces of same dimension\<close>
@@ -6381,7 +6382,7 @@
by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
qed
-proposition isometries_subspaces:
+proposition%important isometries_subspaces:
fixes S :: "'a::euclidean_space set"
and T :: "'b::euclidean_space set"
assumes S: "subspace S"
@@ -6392,7 +6393,7 @@
"\<And>x. x \<in> T \<Longrightarrow> norm(g x) = norm x"
"\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
"\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
-proof -
+proof%unimportant -
obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
and "independent B" "finite B" "card B = dim S" "span B = S"
@@ -6549,7 +6550,7 @@
subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close>
-locale Retracts =
+locale%important Retracts =
fixes s h t k
assumes conth: "continuous_on s h"
and imh: "h ` s = t"
@@ -6715,7 +6716,7 @@
subsection\<open>Homotopy equivalence\<close>
-definition homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
+definition%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
(infix "homotopy'_eqv" 50)
where "S homotopy_eqv T \<equiv>
\<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
@@ -7003,7 +7004,7 @@
shows "\<lbrakk>contractible S; S homeomorphic T\<rbrakk> \<Longrightarrow> contractible T"
by (metis homeomorphic_contractible_eq)
-subsection\<open>Misc other results\<close>
+subsection%unimportant\<open>Misc other results\<close>
lemma bounded_connected_Compl_real:
fixes S :: "real set"
@@ -7047,7 +7048,7 @@
by blast
qed
-subsection\<open>Some Uncountable Sets\<close>
+subsection%unimportant\<open>Some Uncountable Sets\<close>
lemma uncountable_closed_segment:
fixes a :: "'a::real_normed_vector"
@@ -7186,7 +7187,7 @@
by (simp add: arc_imp_simple_path assms simple_path_image_uncountable)
-subsection\<open> Some simple positive connection theorems\<close>
+subsection%unimportant\<open> Some simple positive connection theorems\<close>
proposition path_connected_convex_diff_countable:
fixes U :: "'a::euclidean_space set"
@@ -7453,7 +7454,7 @@
subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
-subsubsection\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
+subsubsection%unimportant\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
lemma homeomorphism_moving_point_1:
fixes a :: "'a::euclidean_space"
@@ -7845,7 +7846,7 @@
qed
qed
-proposition homeomorphism_moving_points_exists:
+proposition%important 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"
@@ -7853,7 +7854,7 @@
and S: "S \<subseteq> T" "T \<subseteq> affine hull S" "connected S"
obtains f g where "homeomorphism T T f g" "\<And>i. i \<in> K \<Longrightarrow> f(x i) = y i"
"{x. ~ (f x = x \<and> g x = x)} \<subseteq> S" "bounded {x. (~ (f x = x \<and> g x = x))}"
-proof (cases "S = {}")
+proof%unimportant (cases "S = {}")
case True
then show ?thesis
using KS homeomorphism_ident that by fastforce
@@ -7875,7 +7876,7 @@
qed
-subsubsection\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
+subsubsection%unimportant\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
lemma homeomorphism_grouping_point_1:
fixes a::real and c::real
@@ -8112,12 +8113,12 @@
qed
qed
-proposition homeomorphism_grouping_points_exists:
+proposition%important 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. (~ (f x = x \<and> g x = x))} \<subseteq> S"
"bounded {x. (~ (f x = x \<and> g x = x))}" "\<And>x. x \<in> K \<Longrightarrow> f x \<in> U"
-proof (cases "2 \<le> DIM('a)")
+proof%unimportant (cases "2 \<le> DIM('a)")
case True
have TS: "T \<subseteq> affine hull S"
using affine_hull_open assms by blast
@@ -8401,13 +8402,13 @@
qed
qed
-proposition nullhomotopic_from_sphere_extension:
+proposition%important nullhomotopic_from_sphere_extension:
fixes f :: "'M::euclidean_space \<Rightarrow> 'a::real_normed_vector"
shows "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
(\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
(\<forall>x \<in> sphere a r. g x = f x))"
(is "?lhs = ?rhs")
-proof (cases r "0::real" rule: linorder_cases)
+proof%unimportant (cases r "0::real" rule: linorder_cases)
case less
then show ?thesis by simp
next
--- a/src/HOL/Analysis/Product_Vector.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Product_Vector.thy Fri Apr 06 17:34:50 2018 +0200
@@ -12,7 +12,7 @@
subsection \<open>Product is a real vector space\<close>
-instantiation prod :: (real_vector, real_vector) real_vector
+instantiation%important prod :: (real_vector, real_vector) real_vector
begin
definition scaleR_prod_def:
@@ -46,10 +46,10 @@
(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
-instantiation prod :: (metric_space, metric_space) dist
+instantiation%important prod :: (metric_space, metric_space) dist
begin
-definition dist_prod_def[code del]:
+definition%important dist_prod_def[code del]:
"dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
instance ..
@@ -68,7 +68,7 @@
declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
-instantiation prod :: (metric_space, metric_space) metric_space
+instantiation%important prod :: (metric_space, metric_space) metric_space
begin
lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
@@ -186,8 +186,8 @@
subsection \<open>Product is a complete metric space\<close>
-instance prod :: (complete_space, complete_space) complete_space
-proof
+instance%important prod :: (complete_space, complete_space) complete_space
+proof%unimportant
fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
have 1: "(\<lambda>n. fst (X n)) \<longlonglongrightarrow> lim (\<lambda>n. fst (X n))"
using Cauchy_fst [OF \<open>Cauchy X\<close>]
@@ -203,7 +203,7 @@
subsection \<open>Product is a normed vector space\<close>
-instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
+instantiation%important prod :: (real_normed_vector, real_normed_vector) real_normed_vector
begin
definition norm_prod_def[code del]:
@@ -245,13 +245,13 @@
instance prod :: (banach, banach) banach ..
-subsubsection \<open>Pair operations are linear\<close>
+subsubsection%unimportant \<open>Pair operations are linear\<close>
-lemma bounded_linear_fst: "bounded_linear fst"
+lemma%important bounded_linear_fst: "bounded_linear fst"
using fst_add fst_scaleR
by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
-lemma bounded_linear_snd: "bounded_linear snd"
+lemma%important bounded_linear_snd: "bounded_linear snd"
using snd_add snd_scaleR
by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
@@ -285,12 +285,12 @@
then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
qed
-subsubsection \<open>Frechet derivatives involving pairs\<close>
+subsubsection%unimportant \<open>Frechet derivatives involving pairs\<close>
-lemma has_derivative_Pair [derivative_intros]:
+lemma%important has_derivative_Pair [derivative_intros]:
assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
-proof (rule has_derivativeI_sandwich[of 1])
+proof%unimportant (rule has_derivativeI_sandwich[of 1])
show "bounded_linear (\<lambda>h. (f' h, g' h))"
using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
@@ -319,7 +319,7 @@
unfolding split_beta' .
-subsubsection \<open>Vector derivatives involving pairs\<close>
+subsubsection%unimportant \<open>Vector derivatives involving pairs\<close>
lemma has_vector_derivative_Pair[derivative_intros]:
assumes "(f has_vector_derivative f') (at x within s)"
@@ -331,7 +331,7 @@
subsection \<open>Product is an inner product space\<close>
-instantiation prod :: (real_inner, real_inner) real_inner
+instantiation%important prod :: (real_inner, real_inner) real_inner
begin
definition inner_prod_def:
--- a/src/HOL/Analysis/Sigma_Algebra.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Fri Apr 06 17:34:50 2018 +0200
@@ -5,7 +5,7 @@
translated by Lawrence Paulson.
*)
-section \<open>Describing measurable sets\<close>
+section \<open>Sigma Algebra\<close>
theory Sigma_Algebra
imports
@@ -27,7 +27,7 @@
subsection \<open>Families of sets\<close>
-locale subset_class =
+locale%important subset_class =
fixes \<Omega> :: "'a set" and M :: "'a set set"
assumes space_closed: "M \<subseteq> Pow \<Omega>"
@@ -36,7 +36,7 @@
subsubsection \<open>Semiring of sets\<close>
-locale semiring_of_sets = subset_class +
+locale%important semiring_of_sets = subset_class +
assumes empty_sets[iff]: "{} \<in> M"
assumes Int[intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
assumes Diff_cover:
@@ -71,7 +71,9 @@
with assms show ?thesis by auto
qed
-locale ring_of_sets = semiring_of_sets +
+subsubsection \<open>Ring of sets\<close>
+
+locale%important ring_of_sets = semiring_of_sets +
assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
lemma (in ring_of_sets) finite_Union [intro]:
@@ -135,20 +137,22 @@
with assms show ?thesis by auto
qed
-locale algebra = ring_of_sets +
+subsubsection \<open>Algebra of sets\<close>
+
+locale%important algebra = ring_of_sets +
assumes top [iff]: "\<Omega> \<in> M"
lemma (in algebra) compl_sets [intro]:
"a \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
by auto
-lemma algebra_iff_Un:
+lemma%important algebra_iff_Un:
"algebra \<Omega> M \<longleftrightarrow>
M \<subseteq> Pow \<Omega> \<and>
{} \<in> M \<and>
(\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
(\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
-proof
+proof%unimportant
assume "algebra \<Omega> M"
then interpret algebra \<Omega> M .
show ?Un using sets_into_space by auto
@@ -169,12 +173,12 @@
show "algebra \<Omega> M" proof qed fact
qed
-lemma algebra_iff_Int:
+lemma%important algebra_iff_Int:
"algebra \<Omega> M \<longleftrightarrow>
M \<subseteq> Pow \<Omega> & {} \<in> M &
(\<forall>a \<in> M. \<Omega> - a \<in> M) &
(\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
-proof
+proof%unimportant
assume "algebra \<Omega> M"
then interpret algebra \<Omega> M .
show ?Int using sets_into_space by auto
@@ -214,7 +218,7 @@
"X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
by (auto simp: algebra_iff_Int)
-subsubsection \<open>Restricted algebras\<close>
+subsubsection%unimportant \<open>Restricted algebras\<close>
abbreviation (in algebra)
"restricted_space A \<equiv> ((\<inter>) A) ` M"
@@ -225,7 +229,7 @@
subsubsection \<open>Sigma Algebras\<close>
-locale sigma_algebra = algebra +
+locale%important sigma_algebra = algebra +
assumes countable_nat_UN [intro]: "\<And>A. range A \<subseteq> M \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
lemma (in algebra) is_sigma_algebra:
@@ -423,7 +427,7 @@
shows "sigma_algebra S { {}, X, S - X, S }"
using algebra.is_sigma_algebra[OF algebra_single_set[OF \<open>X \<subseteq> S\<close>]] by simp
-subsubsection \<open>Binary Unions\<close>
+subsubsection%unimportant \<open>Binary Unions\<close>
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
where "binary a b = (\<lambda>x. b)(0 := a)"
@@ -447,10 +451,10 @@
subsubsection \<open>Initial Sigma Algebra\<close>
-text \<open>Sigma algebras can naturally be created as the closure of any set of
+text%important \<open>Sigma algebras can naturally be created as the closure of any set of
M with regard to the properties just postulated.\<close>
-inductive_set sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
+inductive_set%important sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
for sp :: "'a set" and A :: "'a set set"
where
Basic[intro, simp]: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A"
@@ -796,7 +800,7 @@
thus "(\<Union>i::nat. A i) \<in> M" by (simp add: UN_disjointed_eq)
qed
-subsubsection \<open>Ring generated by a semiring\<close>
+subsubsection%unimportant \<open>Ring generated by a semiring\<close>
definition (in semiring_of_sets)
"generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
@@ -927,7 +931,7 @@
by (blast intro!: sigma_sets_mono elim: generated_ringE)
qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
-subsubsection \<open>A Two-Element Series\<close>
+subsubsection%unimportant \<open>A Two-Element Series\<close>
definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set"
where "binaryset A B = (\<lambda>x. {})(0 := A, Suc 0 := B)"
@@ -943,7 +947,7 @@
subsubsection \<open>Closed CDI\<close>
-definition closed_cdi where
+definition%important closed_cdi where
"closed_cdi \<Omega> M \<longleftrightarrow>
M \<subseteq> Pow \<Omega> &
(\<forall>s \<in> M. \<Omega> - s \<in> M) &
@@ -1177,7 +1181,7 @@
subsubsection \<open>Dynkin systems\<close>
-locale dynkin_system = subset_class +
+locale%important dynkin_system = subset_class +
assumes space: "\<Omega> \<in> M"
and compl[intro!]: "\<And>A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M"
and UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> M
@@ -1239,7 +1243,7 @@
subsubsection "Intersection sets systems"
-definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
+definition%important "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
lemma (in algebra) Int_stable: "Int_stable M"
unfolding Int_stable_def by auto
@@ -1279,7 +1283,7 @@
subsubsection "Smallest Dynkin systems"
-definition dynkin where
+definition%important dynkin where
"dynkin \<Omega> M = (\<Inter>{D. dynkin_system \<Omega> D \<and> M \<subseteq> D})"
lemma dynkin_system_dynkin:
@@ -1426,10 +1430,10 @@
subsubsection \<open>Induction rule for intersection-stable generators\<close>
-text \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
+text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
generated by a generator closed under intersection.\<close>
-lemma sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
+lemma%important sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
assumes "Int_stable G"
and closed: "G \<subseteq> Pow \<Omega>"
and A: "A \<in> sigma_sets \<Omega> G"
@@ -1438,7 +1442,7 @@
and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
shows "P A"
-proof -
+proof%unimportant -
let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
using closed by (rule sigma_algebra_sigma_sets)
@@ -1452,34 +1456,34 @@
subsection \<open>Measure type\<close>
-definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition%important positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"positive M \<mu> \<longleftrightarrow> \<mu> {} = 0"
-definition countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition%important countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
(\<Sum>i. f (A i)) = f (\<Union>i. A i))"
-definition measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition%important measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
"measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
-typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
-proof
+typedef%important 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
+proof%unimportant
have "sigma_algebra UNIV {{}, UNIV}"
by (auto simp: sigma_algebra_iff2)
then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} "
by (auto simp: measure_space_def positive_def countably_additive_def)
qed
-definition space :: "'a measure \<Rightarrow> 'a set" where
+definition%important space :: "'a measure \<Rightarrow> 'a set" where
"space M = fst (Rep_measure M)"
-definition sets :: "'a measure \<Rightarrow> 'a set set" where
+definition%important sets :: "'a measure \<Rightarrow> 'a set set" where
"sets M = fst (snd (Rep_measure M))"
-definition emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
+definition%important emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal" where
"emeasure M = snd (snd (Rep_measure M))"
-definition measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
+definition%important measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
"measure M A = enn2real (emeasure M A)"
declare [[coercion sets]]
@@ -1494,7 +1498,7 @@
interpretation sets: sigma_algebra "space M" "sets M" for M :: "'a measure"
using measure_space[of M] by (auto simp: measure_space_def)
-definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
+definition%important measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
"measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
\<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"
@@ -1629,12 +1633,12 @@
subsubsection \<open>Constructing simple @{typ "'a measure"}\<close>
-lemma emeasure_measure_of:
+lemma%important emeasure_measure_of:
assumes M: "M = measure_of \<Omega> A \<mu>"
assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
assumes X: "X \<in> sets M"
shows "emeasure M X = \<mu> X"
-proof -
+proof%unimportant -
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)
@@ -1711,7 +1715,7 @@
subsubsection \<open>Measurable functions\<close>
-definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
+definition%important measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
"measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
lemma measurableI:
@@ -1873,7 +1877,7 @@
subsubsection \<open>Counting space\<close>
-definition count_space :: "'a set \<Rightarrow> 'a measure" where
+definition%important count_space :: "'a set \<Rightarrow> 'a measure" where
"count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then of_nat (card A) else \<infinity>)"
lemma
@@ -1949,7 +1953,7 @@
"space N = {} \<Longrightarrow> f \<in> measurable M N \<longleftrightarrow> space M = {}"
by (auto simp add: measurable_def Pi_iff)
-subsubsection \<open>Extend measure\<close>
+subsubsection%unimportant \<open>Extend measure\<close>
definition "extend_measure \<Omega> I G \<mu> =
(if (\<exists>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') \<and> \<not> (\<forall>i\<in>I. \<mu> i = 0)
@@ -2011,7 +2015,7 @@
subsection \<open>The smallest $\sigma$-algebra regarding a function\<close>
-definition
+definition%important
"vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"
lemma space_vimage_algebra[simp]: "space (vimage_algebra X f M) = X"
--- a/src/HOL/Analysis/Starlike.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Starlike.thy Fri Apr 06 17:34:50 2018 +0200
@@ -15,7 +15,7 @@
subsection \<open>Midpoint\<close>
-definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
+definition%important midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
lemma midpoint_idem [simp]: "midpoint x x = x"
@@ -94,10 +94,10 @@
subsection \<open>Line segments\<close>
-definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
+definition%important closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
-definition open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
+definition%important open_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
"open_segment a b \<equiv> closed_segment a b - {a,b}"
lemmas segment = open_segment_def closed_segment_def
@@ -599,7 +599,7 @@
subsection\<open>Starlike sets\<close>
-definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
+definition%important "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
lemma starlike_UNIV [simp]: "starlike UNIV"
by (simp add: starlike_def)
@@ -662,7 +662,7 @@
by (meson hull_mono inf_mono subset_insertI subset_refl)
qed
-subsection\<open>More results about segments\<close>
+subsection%unimportant\<open>More results about segments\<close>
lemma dist_half_times2:
fixes a :: "'a :: real_normed_vector"
@@ -884,7 +884,7 @@
subsection\<open>Betweenness\<close>
-definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
+definition%important "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
lemma betweenI:
assumes "0 \<le> u" "u \<le> 1" "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
@@ -1055,7 +1055,7 @@
by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
-subsection \<open>Shrinking towards the interior of a convex set\<close>
+subsection%unimportant \<open>Shrinking towards the interior of a convex set\<close>
lemma mem_interior_convex_shrink:
fixes s :: "'a::euclidean_space set"
@@ -1249,7 +1249,7 @@
qed
-subsection \<open>Some obvious but surprisingly hard simplex lemmas\<close>
+subsection%unimportant \<open>Some obvious but surprisingly hard simplex lemmas\<close>
lemma simplex:
assumes "finite s"
@@ -1693,7 +1693,7 @@
qed
-subsection \<open>Relative interior of convex set\<close>
+subsection%unimportant \<open>Relative interior of convex set\<close>
lemma rel_interior_convex_nonempty_aux:
fixes S :: "'n::euclidean_space set"
@@ -2081,7 +2081,7 @@
subsection\<open>The relative frontier of a set\<close>
-definition "rel_frontier S = closure S - rel_interior S"
+definition%important "rel_frontier S = closure S - rel_interior S"
lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
by (simp add: rel_frontier_def)
@@ -2460,7 +2460,7 @@
qed
-subsubsection \<open>Relative interior and closure under common operations\<close>
+subsubsection%unimportant \<open>Relative interior and closure under common operations\<close>
lemma rel_interior_inter_aux: "\<Inter>{rel_interior S |S. S \<in> I} \<subseteq> \<Inter>I"
proof -
@@ -3150,7 +3150,7 @@
by (force simp: rel_frontier_def rel_interior_Times assms closure_Times)
-subsubsection \<open>Relative interior of convex cone\<close>
+subsubsection%unimportant \<open>Relative interior of convex cone\<close>
lemma cone_rel_interior:
fixes S :: "'m::euclidean_space set"
@@ -3423,7 +3423,7 @@
qed
-subsection \<open>Convexity on direct sums\<close>
+subsection%unimportant \<open>Convexity on direct sums\<close>
lemma closure_sum:
fixes S T :: "'a::real_normed_vector set"
@@ -3794,7 +3794,7 @@
using \<open>y < x\<close> by (simp add: field_simps)
qed simp
-subsection\<open>Explicit formulas for interior and relative interior of convex hull\<close>
+subsection%unimportant\<open>Explicit formulas for interior and relative interior of convex hull\<close>
lemma at_within_cbox_finite:
assumes "x \<in> box a b" "x \<notin> S" "finite S"
@@ -4157,7 +4157,7 @@
by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
qed
-subsection\<open>Similar results for closure and (relative or absolute) frontier.\<close>
+subsection%unimportant\<open>Similar results for closure and (relative or absolute) frontier.\<close>
lemma closure_convex_hull [simp]:
fixes s :: "'a::euclidean_space set"
@@ -4315,7 +4315,7 @@
subsection \<open>Coplanarity, and collinearity in terms of affine hull\<close>
-definition coplanar where
+definition%important coplanar where
"coplanar s \<equiv> \<exists>u v w. s \<subseteq> affine hull {u,v,w}"
lemma collinear_affine_hull:
@@ -4767,7 +4767,7 @@
subsection\<open>The infimum of the distance between two sets\<close>
-definition setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
+definition%important setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
"setdist s t \<equiv>
(if s = {} \<or> t = {} then 0
else Inf {dist x y| x y. x \<in> s \<and> y \<in> t})"
@@ -5003,7 +5003,7 @@
\<Longrightarrow> setdist {x} S > 0"
using less_eq_real_def setdist_eq_0_closedin by fastforce
-subsection\<open>Basic lemmas about hyperplanes and halfspaces\<close>
+subsection%unimportant\<open>Basic lemmas about hyperplanes and halfspaces\<close>
lemma hyperplane_eq_Ex:
assumes "a \<noteq> 0" obtains x where "a \<bullet> x = b"
@@ -5056,7 +5056,7 @@
using halfspace_eq_empty_le [of "-a" "-b"]
by simp
-subsection\<open>Use set distance for an easy proof of separation properties\<close>
+subsection%unimportant\<open>Use set distance for an easy proof of separation properties\<close>
proposition separation_closures:
fixes S :: "'a::euclidean_space set"
@@ -5150,12 +5150,12 @@
subsection\<open>Connectedness of the intersection of a chain\<close>
-proposition connected_chain:
+proposition%important connected_chain:
fixes \<F> :: "'a :: euclidean_space set set"
assumes cc: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S \<and> connected S"
and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
shows "connected(\<Inter>\<F>)"
-proof (cases "\<F> = {}")
+proof%unimportant (cases "\<F> = {}")
case True then show ?thesis
by auto
next
@@ -5299,13 +5299,13 @@
by (meson le_max_iff_disj)
qed
-proposition proper_map:
+proposition%important proper_map:
fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
assumes "closedin (subtopology euclidean S) K"
and com: "\<And>U. \<lbrakk>U \<subseteq> T; compact U\<rbrakk> \<Longrightarrow> compact (S \<inter> f -` U)"
and "f ` S \<subseteq> T"
shows "closedin (subtopology euclidean T) (f ` K)"
-proof -
+proof%unimportant -
have "K \<subseteq> S"
using assms closedin_imp_subset by metis
obtain C where "closed C" and Keq: "K = S \<inter> C"
@@ -5387,7 +5387,7 @@
by (simp add: continuous_on_closed * closedin_imp_subset)
qed
-subsection\<open>Trivial fact: convexity equals connectedness for collinear sets\<close>
+subsection%unimportant\<open>Trivial fact: convexity equals connectedness for collinear sets\<close>
lemma convex_connected_collinear:
fixes S :: "'a::euclidean_space set"
@@ -5605,7 +5605,7 @@
by (simp add: clo closedin_closed_Int)
qed
-subsubsection\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
+subsubsection%unimportant\<open>Representing affine hull as a finite intersection of hyperplanes\<close>
proposition affine_hull_convex_Int_nonempty_interior:
fixes S :: "'a::real_normed_vector set"
@@ -5778,7 +5778,7 @@
(if a = 0 \<and> r > 0 then -1 else DIM('a))"
using aff_dim_halfspace_le [of "-a" "-r"] by simp
-subsection\<open>Properties of special hyperplanes\<close>
+subsection%unimportant\<open>Properties of special hyperplanes\<close>
lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}"
by (simp add: subspace_def inner_right_distrib)
@@ -5925,7 +5925,7 @@
shows "a \<noteq> 0 \<Longrightarrow> aff_dim {x. a \<bullet> x = r} = DIM('a) - 1"
by (metis aff_dim_eq_hyperplane affine_hull_eq affine_hyperplane)
-subsection\<open>Some stepping theorems\<close>
+subsection%unimportant\<open>Some stepping theorems\<close>
lemma dim_empty [simp]: "dim ({} :: 'a::euclidean_space set) = 0"
by (force intro!: dim_unique)
@@ -6092,7 +6092,7 @@
by (metis One_nat_def \<open>a \<noteq> 0\<close> affine_bounded_eq_lowdim affine_hyperplane bounded_hyperplane_eq_trivial_0)
qed
-subsection\<open>General case without assuming closure and getting non-strict separation\<close>
+subsection%unimportant\<open>General case without assuming closure and getting non-strict separation\<close>
proposition separating_hyperplane_closed_point_inset:
fixes S :: "'a::euclidean_space set"
@@ -6280,7 +6280,7 @@
by (metis assms convex_closure convex_rel_interior_closure)
-subsection\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
+subsection%unimportant\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
lemma
fixes s :: "'a::euclidean_space set"
@@ -6636,7 +6636,7 @@
qed
qed
-subsection\<open>Misc results about span\<close>
+subsection%unimportant\<open>Misc results about span\<close>
lemma eq_span_insert_eq:
assumes "(x - y) \<in> span S"
@@ -7026,11 +7026,11 @@
apply (simp add: x)
done
-proposition Gram_Schmidt_step:
+proposition%important Gram_Schmidt_step:
fixes S :: "'a::euclidean_space set"
assumes S: "pairwise orthogonal S" and x: "x \<in> span S"
shows "orthogonal x (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b))"
-proof -
+proof%unimportant -
have "finite S"
by (simp add: S pairwise_orthogonal_imp_finite)
have "orthogonal (a - (\<Sum>b\<in>S. (b \<bullet> a / (b \<bullet> b)) *\<^sub>R b)) x"
@@ -7087,11 +7087,11 @@
qed
-proposition orthogonal_extension:
+proposition%important orthogonal_extension:
fixes S :: "'a::euclidean_space set"
assumes S: "pairwise orthogonal S"
obtains U where "pairwise orthogonal (S \<union> U)" "span (S \<union> U) = span (S \<union> T)"
-proof -
+proof%unimportant -
obtain B where "finite B" "span B = span T"
using basis_subspace_exists [of "span T"] subspace_span by auto
with orthogonal_extension_aux [of B S]
@@ -7149,13 +7149,13 @@
done
qed
-proposition orthonormal_basis_subspace:
+proposition%important orthonormal_basis_subspace:
fixes S :: "'a :: euclidean_space set"
assumes "subspace S"
obtains B where "B \<subseteq> S" "pairwise orthogonal B"
and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
and "independent B" "card B = dim S" "span B = S"
-proof -
+proof%unimportant -
obtain B where "0 \<notin> B" "B \<subseteq> S"
and orth: "pairwise orthogonal B"
and "independent B" "card B = dim S" "span B = S"
@@ -7186,11 +7186,11 @@
qed
-proposition orthogonal_to_subspace_exists_gen:
+proposition%important orthogonal_to_subspace_exists_gen:
fixes S :: "'a :: euclidean_space set"
assumes "span S \<subset> span T"
obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
-proof -
+proof%unimportant -
obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
and "independent B" "card B = dim S" "span B = span S"
@@ -7249,10 +7249,10 @@
by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_clauses(1) that)
qed
-proposition orthogonal_subspace_decomp_exists:
+proposition%important orthogonal_subspace_decomp_exists:
fixes S :: "'a :: euclidean_space set"
obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
-proof -
+proof%unimportant -
obtain T where "0 \<notin> T" "T \<subseteq> span S" "pairwise orthogonal T" "independent T" "card T = dim (span S)" "span T = span S"
using orthogonal_basis_subspace subspace_span by blast
let ?a = "\<Sum>b\<in>T. (b \<bullet> x / (b \<bullet> b)) *\<^sub>R b"
@@ -7341,11 +7341,11 @@
qed
qed
-proposition dim_orthogonal_sum:
+proposition%important dim_orthogonal_sum:
fixes A :: "'a::euclidean_space set"
assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
shows "dim(A \<union> B) = dim A + dim B"
-proof -
+proof%unimportant -
have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
@@ -7472,10 +7472,10 @@
subsection\<open>Lower-dimensional affine subsets are nowhere dense.\<close>
-proposition dense_complement_subspace:
+proposition%important dense_complement_subspace:
fixes S :: "'a :: euclidean_space set"
assumes dim_less: "dim T < dim S" and "subspace S" shows "closure(S - T) = S"
-proof -
+proof%unimportant -
have "closure(S - U) = S" if "dim U < dim S" "U \<subseteq> S" for U
proof -
have "span U \<subset> span S"
@@ -7583,7 +7583,7 @@
by (simp add: assms dense_complement_convex)
-subsection\<open>Parallel slices, etc.\<close>
+subsection%unimportant\<open>Parallel slices, etc.\<close>
text\<open> If we take a slice out of a set, we can do it perpendicularly,
with the normal vector to the slice parallel to the affine hull.\<close>
@@ -7811,7 +7811,7 @@
subsection\<open>Several Variants of Paracompactness\<close>
-proposition paracompact:
+proposition%important paracompact:
fixes S :: "'a :: euclidean_space set"
assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
obtains \<C>' where "S \<subseteq> \<Union> \<C>'"
@@ -7819,7 +7819,7 @@
and "\<And>x. x \<in> S
\<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and>
finite {U. U \<in> \<C>' \<and> (U \<inter> V \<noteq> {})}"
-proof (cases "S = {}")
+proof%unimportant (cases "S = {}")
case True with that show ?thesis by blast
next
case False
@@ -7955,7 +7955,7 @@
using paracompact_closedin [of UNIV S \<C>] assms by auto
-subsection\<open>Closed-graph characterization of continuity\<close>
+subsection%unimportant\<open>Closed-graph characterization of continuity\<close>
lemma continuous_closed_graph_gen:
fixes T :: "'b::real_normed_vector set"
@@ -8026,7 +8026,7 @@
by (rule continuous_on_Un_local_open [OF opS opT])
qed
-subsection\<open>The union of two collinear segments is another segment\<close>
+subsection%unimportant\<open>The union of two collinear segments is another segment\<close>
proposition in_convex_hull_exchange:
fixes a :: "'a::euclidean_space"
@@ -8204,14 +8204,14 @@
subsection\<open>Covering an open set by a countable chain of compact sets\<close>
-proposition open_Union_compact_subsets:
+proposition%important open_Union_compact_subsets:
fixes S :: "'a::euclidean_space set"
assumes "open S"
obtains C where "\<And>n. compact(C n)" "\<And>n. C n \<subseteq> S"
"\<And>n. C n \<subseteq> interior(C(Suc n))"
"\<Union>(range C) = S"
"\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. K \<subseteq> (C n)"
-proof (cases "S = {}")
+proof%unimportant (cases "S = {}")
case True
then show ?thesis
by (rule_tac C = "\<lambda>n. {}" in that) auto
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Apr 05 06:15:02 2018 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Apr 06 17:34:50 2018 +0200
@@ -131,7 +131,7 @@
context topological_space
begin
-definition "topological_basis B \<longleftrightarrow>
+definition%important "topological_basis B \<longleftrightarrow>
(\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
lemma topological_basis:
@@ -257,7 +257,7 @@
subsection \<open>Countable Basis\<close>
-locale countable_basis =
+locale%important countable_basis =
fixes B :: "'a::topological_space set set"
assumes is_basis: "topological_basis B"
and countable_basis: "countable B"
@@ -578,19 +578,19 @@
then show ?thesis using B(1) by auto
qed
-subsection \<open>Polish spaces\<close>
+subsection%important \<open>Polish spaces\<close>
text \<open>Textbooks define Polish spaces as completely metrizable.
We assume the topology to be complete for a given metric.\<close>
-class polish_space = complete_space + second_countable_topology
+class%important polish_space = complete_space + second_countable_topology
subsection \<open>General notion of a topology as a value\<close>
-definition "istopology L \<longleftrightarrow>
+definition%important "istopology L \<longleftrightarrow>
L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
-typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
+typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
morphisms "openin" "topology"
unfolding istopology_def by blast
@@ -620,7 +620,7 @@
subsubsection \<open>Main properties of open sets\<close>
-lemma openin_clauses:
+lemma%important openin_clauses:
fixes U :: "'a topology"
shows
"openin U {}"
@@ -683,7 +683,7 @@
subsubsection \<open>Closed sets\<close>
-definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
+definition%important "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
by (metis closedin_def)
@@ -755,7 +755,7 @@
subsubsection \<open>Subspace topology\<close>
-definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
+definition%important "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
(is "istopology ?L")
@@ -870,7 +870,7 @@
subsubsection \<open>The standard Euclidean topology\<close>
-definition euclidean :: "'a::topological_space topology"
+definition%important euclidean :: "'a::topological_space topology"
where "euclidean = topology open"
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
@@ -1054,13 +1054,13 @@
subsection \<open>Open and closed balls\<close>
-definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
where "ball x e = {y. dist x y < e}"
-definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+definition%important cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
where "cball x e = {y. dist x y \<le> e}"
-definition sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+definition%important sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
where "sphere x e = {y. dist x y = e}"
lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
@@ -1327,11 +1327,11 @@
corollary Zero_neq_One[iff]: "0 \<noteq> One"
by (metis One_non_0)
-definition (in euclidean_space) eucl_less (infix "<e" 50)
+definition%important (in euclidean_space) eucl_less (infix "<e" 50)
where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
-definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
-definition "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
+definition%important box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
+definition%important "cbox a b = {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i}"
lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
@@ -1873,9 +1873,9 @@
by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
qed
-text \<open>Intervals in general, including infinite and mixtures of open and closed.\<close>
-
-definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
+subsection \<open>Intervals in general, including infinite and mixtures of open and closed.\<close>
+
+definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
lemma is_interval_1:
@@ -2053,7 +2053,7 @@
subsection \<open>Limit points\<close>
-definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60)
+definition%important (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60)
where "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
lemma islimptI:
@@ -2191,7 +2191,7 @@
subsection \<open>Interior of a Set\<close>
-definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
+definition%important "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
lemma interiorI [intro?]:
assumes "open T" and "x \<in> T" and "T \<subseteq> S"
@@ -2359,7 +2359,7 @@
subsection \<open>Closure of a Set\<close>
-definition "closure S = S \<union> {x | x. x islimpt S}"
+definition%important "closure S = S \<union> {x | x. x islimpt S}"
lemma interior_closure: "interior S = - (closure (- S))"
by (auto simp: interior_def closure_def islimpt_def)
@@ -2635,7 +2635,7 @@
subsection \<open>Frontier (also known as boundary)\<close>
-definition "frontier S = closure S - interior S"
+definition%important "frontier S = closure S - interior S"
lemma frontier_closed [iff]: "closed (frontier S)"
by (simp add: frontier_def closed_Diff)
@@ -2726,7 +2726,7 @@
qed
-subsection \<open>Filters and the ``eventually true'' quantifier\<close>
+subsection%unimportant \<open>Filters and the ``eventually true'' quantifier\<close>
definition indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter" (infixr "indirection" 70)
where "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
@@ -2794,16 +2794,16 @@
subsection \<open>Limits\<close>
-lemma Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
+lemma%important Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
by (auto simp: tendsto_iff trivial_limit_eq)
text \<open>Show that they yield usual definitions in the various cases.\<close>
-lemma Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
+lemma%important Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)"
by (auto simp: tendsto_iff eventually_at_le)
-lemma Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
+lemma%important Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
by (auto simp: tendsto_iff eventually_at)
@@ -2814,11 +2814,11 @@
apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
done
-lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
+lemma%important Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
by (auto simp: tendsto_iff eventually_at)
-lemma Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
+lemma%important Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
by (auto simp: tendsto_iff eventually_at_infinity)
corollary Lim_at_infinityI [intro?]:
@@ -3411,7 +3411,7 @@
subsection \<open>Boundedness\<close>
(* FIXME: This has to be unified with BSEQ!! *)
-definition (in metric_space) bounded :: "'a set \<Rightarrow> bool"
+definition%important (in metric_space) bounded :: "'a set \<Rightarrow> bool"
where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"
@@ -3690,12 +3690,12 @@
subsubsection \<open>Bolzano-Weierstrass property\<close>
-lemma heine_borel_imp_bolzano_weierstrass:
+lemma%important heine_borel_imp_bolzano_weierstrass:
assumes "compact s"
and "infinite t"
and "t \<subseteq> s"
shows "\<exists>x \<in> s. x islimpt t"
-proof (rule ccontr)
+proof%unimportant (rule ccontr)
assume "\<not> (\<exists>x \<in> s. x islimpt t)"
then obtain f where f: "\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)"
unfolding islimpt_def
@@ -4157,7 +4157,7 @@
with \<open>U \<inter> \<Inter>A = {}\<close> show False by auto
qed
-definition "countably_compact U \<longleftrightarrow>
+definition%important "countably_compact U \<longleftrightarrow>
(\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))"
lemma countably_compactE:
@@ -4208,9 +4208,9 @@
unfolding C_def by (intro exI[of _ "f`T"]) fastforce
qed
-lemma countably_compact_imp_compact_second_countable:
+lemma%important countably_compact_imp_compact_second_countable:
"countably_compact U \<Longrightarrow> compact (U :: 'a :: second_countable_topology set)"
-proof (rule countably_compact_imp_compact)
+proof%unimportant (rule countably_compact_imp_compact)
fix T and x :: 'a
assume "open T" "x \<in> T"
from topological_basisE[OF is_basis this] obtain b where
@@ -4225,7 +4225,7 @@
subsubsection\<open>Sequential compactness\<close>
-definition seq_compact :: "'a::topological_space set \<Rightarrow> bool"
+definition%important seq_compact :: "'a::topological_space set \<Rightarrow> bool"
where "seq_compact S \<longleftrightarrow>
(\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
@@ -4486,10 +4486,10 @@
shows "seq_compact U \<longleftrightarrow> compact U"
using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
-lemma bolzano_weierstrass_imp_seq_compact:
+lemma%important bolzano_weierstrass_imp_seq_compact:
fixes s :: "'a::{t1_space, first_countable_topology} set"
shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
- by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
+ by%unimportant (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
subsubsection\<open>Totally bounded\<close>
@@ -4497,10 +4497,10 @@
lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (s m) (s n) < e)"
unfolding Cauchy_def by metis
-lemma seq_compact_imp_totally_bounded:
+lemma%important seq_compact_imp_totally_bounded:
assumes "seq_compact s"
shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
-proof -
+proof%unimportant -
{ fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"
let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
@@ -4529,11 +4529,11 @@
subsubsection\<open>Heine-Borel theorem\<close>
-lemma seq_compact_imp_heine_borel:
+lemma%important seq_compact_imp_heine_borel:
fixes s :: "'a :: metric_space set"
assumes "seq_compact s"
shows "compact s"
-proof -
+proof%unimportant -
from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>]
obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)"
unfolding choice_iff' ..
@@ -4574,22 +4574,22 @@
qed
qed
-lemma compact_eq_seq_compact_metric:
+lemma%important compact_eq_seq_compact_metric:
"compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
-lemma compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
+lemma%important compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
"compact (S :: 'a::metric_space set) \<longleftrightarrow>
(\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
unfolding compact_eq_seq_compact_metric seq_compact_def by auto
subsubsection \<open>Complete the chain of compactness variants\<close>
-lemma compact_eq_bolzano_weierstrass:
+lemma%important compact_eq_bolzano_weierstrass:
fixes s :: "'a::metric_space set"
shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"
(is "?lhs = ?rhs")
-proof
+proof%unimportant
assume ?lhs
then show ?rhs
using heine_borel_imp_bolzano_weierstrass[of s] by auto
@@ -4599,7 +4599,7 @@
unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
qed
-lemma bolzano_weierstrass_imp_bounded:
+lemma%important bolzano_weierstrass_imp_bounded:
"\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
@@ -4611,16 +4611,16 @@
Heine-Borel property if every closed and bounded subset is compact.
\<close>
-class heine_borel = metric_space +
+class%important heine_borel = metric_space +
assumes bounded_imp_convergent_subsequence:
"bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
-lemma bounded_closed_imp_seq_compact:
+lemma%important bounded_closed_imp_seq_compact:
fixes s::"'a::heine_borel set"
assumes "bounded s"
and "closed s"
shows "seq_compact s"
-proof (unfold seq_compact_def, clarify)
+proof%unimportant (unfold seq_compact_def, clarify)
fix f :: "nat \<Rightarrow> 'a"
assume f: "\<forall>n. f n \<in> s"
with \<open>bounded s\<close> have "bounded (range f)"
@@ -4690,8 +4690,8 @@
by (metis of_nat_le_iff Int_subset_iff \<open>K \<subseteq> S\<close> real_arch_simple subset_cball subset_trans)
qed auto
-instance real :: heine_borel
-proof
+instance%important real :: heine_borel
+proof%unimportant
fix f :: "nat \<Rightarrow> real"
assume f: "bounded (range f)"
obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)"
@@ -4771,8 +4771,8 @@
(auto intro!: assms bounded_linear_inner_left bounded_linear_image
simp: euclidean_representation)
-instance euclidean_space \<subseteq> heine_borel
-proof
+instance%important euclidean_space \<subseteq> heine_borel
+proof%unimportant
fix f :: "nat \<Rightarrow> 'a"
assume f: "bounded (range f)"
then obtain l::'a and r where r: "strict_mono r"
@@ -4818,8 +4818,8 @@
unfolding bounded_def
by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)
-instance prod :: (heine_borel, heine_borel) heine_borel
-proof
+instance%important prod :: (heine_borel, heine_borel) heine_borel
+proof%unimportant
fix f :: "nat \<Rightarrow> 'a \<times> 'b"
assume f: "bounded (range f)"
then have "bounded (fst ` range f)"
@@ -4845,12 +4845,12 @@
subsubsection \<open>Completeness\<close>
-lemma (in metric_space) completeI:
+lemma%important (in metric_space) completeI:
assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
shows "complete s"
using assms unfolding complete_def by fast
-lemma (in metric_space) completeE:
+lemma%important (in metric_space) completeE:
assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
using assms unfolding complete_def by fast
@@ -4900,10 +4900,10 @@
then show ?thesis unfolding complete_def by auto
qed
-lemma compact_eq_totally_bounded:
+lemma%important compact_eq_totally_bounded:
"compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
(is "_ \<longleftrightarrow> ?rhs")
-proof
+proof%unimportant
assume assms: "?rhs"
then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)"
by (auto simp: choice_iff')
@@ -5107,7 +5107,7 @@
text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
-lemma continuous_within_eps_delta:
+lemma%important continuous_within_eps_delta:
"continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s. dist x' x < d --> dist (f x') (f x) < e)"
unfolding continuous_within and Lim_within by fastforce
@@ -5435,7 +5435,7 @@
by (force intro: Lim_transform_within)
-subsubsection \<open>Structural rules for pointwise continuity\<close>
+subsubsection%unimportant \<open>Structural rules for pointwise continuity\<close>
lemma continuous_infnorm[continuous_intros]:
"continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
@@ -5447,7 +5447,7 @@
shows "continuous F (\<lambda>x. inner (f x) (g x))"
using assms unfolding continuous_def by (rule tendsto_inner)
-subsubsection \<open>Structural rules for setwise continuity\<close>
+subsubsection%unimportant \<open>Structural rules for setwise continuity\<close>
lemma continuous_on_infnorm[continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
@@ -5461,7 +5461,7 @@
using bounded_bilinear_inner assms
by (rule bounded_bilinear.continuous_on)
-subsubsection \<open>Structural rules for uniform continuity\<close>
+subsubsection%unimportant \<open>Structural rules for uniform continuity\<close>
lemma uniformly_continuous_on_dist[continuous_intros]:
fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
@@ -5653,7 +5653,7 @@
shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
using assms continuous_on_closed by blast
-subsection \<open>Half-global and completely global cases.\<close>
+subsection%unimportant \<open>Half-global and completely global cases.\<close>
lemma continuous_openin_preimage_gen:
assumes "continuous_on S f" "open T"
@@ -5743,7 +5743,7 @@
with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
qed
-subsection \<open>Topological properties of linear functions.\<close>
+subsection%unimportant \<open>Topological properties of linear functions.\<close>
lemma linear_lim_0:
assumes "bounded_linear f"
@@ -5771,7 +5771,7 @@
"bounded_linear f \<Longrightarrow> continuous_on s f"
using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
-subsection \<open>Intervals\<close>
+subsection%unimportant \<open>Intervals\<close>
text \<open>Openness of halfspaces.\<close>