--- a/src/HOL/Analysis/Binary_Product_Measure.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Tue Jan 22 22:57:16 2019 +0000
@@ -2,7 +2,7 @@
Author: Johannes Hölzl, TU München
*)
-section%important \<open>Binary Product Measure\<close>
+section \<open>Binary Product Measure\<close>
theory Binary_Product_Measure
imports Nonnegative_Lebesgue_Integration
--- a/src/HOL/Analysis/Bochner_Integration.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Bochner_Integration.thy Tue Jan 22 22:57:16 2019 +0000
@@ -2,7 +2,7 @@
Author: Johannes Hölzl, TU München
*)
-section%important \<open>Bochner Integration for Vector-Valued Functions\<close>
+section \<open>Bochner Integration for Vector-Valued Functions\<close>
theory Bochner_Integration
imports Finite_Product_Measure
--- a/src/HOL/Analysis/Borel_Space.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Borel_Space.thy Tue Jan 22 22:57:16 2019 +0000
@@ -3,7 +3,7 @@
Author: Armin Heller, TU München
*)
-section%important \<open>Borel Space\<close>
+section \<open>Borel Space\<close>
theory Borel_Space
imports
@@ -17,7 +17,7 @@
lemma topological_basis_trivial: "topological_basis {A. open A}"
by (auto simp: topological_basis_def)
-lemma%important open_prod_generated: "open = generate_topology {A \<times> B | A B. open A \<and> open B}"
+proposition open_prod_generated: "open = generate_topology {A \<times> B | A B. open A \<and> open B}"
proof -
have "{A \<times> B :: ('a \<times> 'b) set | A B. open A \<and> open B} = ((\<lambda>(a, b). a \<times> b) ` ({A. open A} \<times> {A. open A}))"
by auto
@@ -509,7 +509,7 @@
shows "borel = sigma UNIV (range (\<lambda>(i, j). F i j))"
using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\<lambda>(i, j). F i j)"]) auto
-lemma second_countable_borel_measurable:
+theorem second_countable_borel_measurable:
fixes X :: "'a::second_countable_topology set set"
assumes eq: "open = generate_topology X"
shows "borel = sigma UNIV X"
@@ -569,7 +569,7 @@
finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
qed simp_all
-lemma borel_eq_countable_basis:
+proposition borel_eq_countable_basis:
fixes B::"'a::topological_space set set"
assumes "countable B"
assumes "topological_basis B"
--- a/src/HOL/Analysis/Caratheodory.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Caratheodory.thy Tue Jan 22 22:57:16 2019 +0000
@@ -3,7 +3,7 @@
Author: Johannes Hölzl, TU München
*)
-section%important \<open>Caratheodory Extension Theorem\<close>
+section \<open>Caratheodory Extension Theorem\<close>
theory Caratheodory
imports Measure_Space
@@ -54,7 +54,7 @@
definition%important outer_measure_space where
"outer_measure_space M f \<longleftrightarrow> positive M f \<and> increasing M f \<and> countably_subadditive M f"
-subsubsection \<open>Lambda Systems\<close>
+subsubsection%important \<open>Lambda Systems\<close>
definition%important lambda_system :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set set"
where
@@ -635,7 +635,7 @@
qed
qed
-subsubsection \<open>Caratheodory on semirings\<close>
+subsubsection%important \<open>Caratheodory on semirings\<close>
theorem (in semiring_of_sets) caratheodory:
assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>"
--- a/src/HOL/Analysis/Extended_Real_Limits.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy Tue Jan 22 22:57:16 2019 +0000
@@ -5,7 +5,7 @@
Author: Bogdan Grechuk, University of Edinburgh
*)
-section%important \<open>Limits on the Extended Real Number Line\<close> (* TO FIX: perhaps put all Nonstandard Analysis related
+section \<open>Limits on the Extended Real Number Line\<close> (* TO FIX: perhaps put all Nonstandard Analysis related
topics together? *)
theory Extended_Real_Limits
@@ -391,7 +391,7 @@
qed
-subsubsection \<open>Continuity of addition\<close>
+subsubsection%important \<open>Continuity of addition\<close>
text \<open>The next few lemmas remove an unnecessary assumption in \<open>tendsto_add_ereal\<close>, culminating
in \<open>tendsto_add_ereal_general\<close> which essentially says that the addition
@@ -522,7 +522,7 @@
then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
qed
-subsubsection \<open>Continuity of multiplication\<close>
+subsubsection%important \<open>Continuity of multiplication\<close>
text \<open>In the same way as for addition, we prove that the multiplication is continuous on
ereal times ereal, except at \<open>(\<infinity>, 0)\<close> and \<open>(-\<infinity>, 0)\<close> and \<open>(0, \<infinity>)\<close> and \<open>(0, -\<infinity>)\<close>,
@@ -659,7 +659,7 @@
by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
-subsubsection \<open>Continuity of division\<close>
+subsubsection%important \<open>Continuity of division\<close>
lemma tendsto_inverse_ereal_PInf:
fixes u::"_ \<Rightarrow> ereal"
--- a/src/HOL/Analysis/Fashoda_Theorem.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Tue Jan 22 22:57:16 2019 +0000
@@ -2,7 +2,7 @@
Author: Robert Himmelmann, TU Muenchen (translation from HOL light)
*)
-section%important \<open>Fashoda Meet Theorem\<close>
+section \<open>Fashoda Meet Theorem\<close>
theory Fashoda_Theorem
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Tue Jan 22 22:57:16 2019 +0000
@@ -2,7 +2,7 @@
Author: Johannes Hölzl, TU München
*)
-section%important \<open>Finite Product Measure\<close>
+section \<open>Finite Product Measure\<close>
theory Finite_Product_Measure
imports Binary_Product_Measure
--- a/src/HOL/Analysis/Function_Topology.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Function_Topology.thy Tue Jan 22 22:57:16 2019 +0000
@@ -7,7 +7,7 @@
begin
-section%important \<open>Product Topology\<close>
+section \<open>Product Topology\<close> (* FIX see comments by the author *)
text \<open>We want to define the product topology.
@@ -63,7 +63,7 @@
subsection \<open>Topology without type classes\<close>
-subsubsection \<open>The topology generated by some (open) subsets\<close>
+subsubsection%important \<open>The topology generated by some (open) subsets\<close>
text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
as it follows from \<open>UN\<close> taking for \<open>K\<close> the empty set. However, it is convenient to have,
@@ -257,7 +257,7 @@
qed
qed
-subsubsection \<open>Continuity\<close>
+subsubsection%important \<open>Continuity\<close>
text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
of type classes, as defined below.\<close>
@@ -335,7 +335,7 @@
using assms unfolding continuous_on_topo_def by auto
-subsubsection \<open>Pullback topology\<close>
+subsubsection%important \<open>Pullback topology\<close>
text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
a special case of this notion, pulling back by the identity. We introduce the general notion as
@@ -808,7 +808,7 @@
qed
-subsubsection \<open>Powers of a single topological space as a topological space, using type classes\<close>
+subsubsection%important \<open>Powers of a single topological space as a topological space, using type classes\<close>
instantiation "fun" :: (type, topological_space) topological_space
begin
@@ -884,7 +884,7 @@
"continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
by (auto intro: continuous_on_product_then_coordinatewise)
-subsubsection \<open>Topological countability for product spaces\<close>
+subsubsection%important \<open>Topological countability for product spaces\<close>
text \<open>The next two lemmas are useful to prove first or second countability
of product spaces, but they have more to do with countability and could
--- a/src/HOL/Analysis/Further_Topology.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy Tue Jan 22 22:57:16 2019 +0000
@@ -1,4 +1,4 @@
-section%important \<open>Extending Continous Maps, Invariance of Domain, etc\<close> (*FIX rename? *)
+section \<open>Extending Continous Maps, Invariance of Domain, etc\<close> (*FIX rename? *)
text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
--- a/src/HOL/Analysis/Great_Picard.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Great_Picard.thy Tue Jan 22 22:57:16 2019 +0000
@@ -1,4 +1,4 @@
-section%important \<open>The Great Picard Theorem and its Applications\<close>
+section \<open>The Great Picard Theorem and its Applications\<close>
text\<open>Ported from HOL Light (cauchy.ml) by L C Paulson, 2017\<close>
@@ -376,7 +376,7 @@
subsection\<open>The Little Picard Theorem\<close>
-proposition Landau_Picard:
+theorem Landau_Picard:
obtains R
where "\<And>z. 0 < R z"
"\<And>f. \<lbrakk>f holomorphic_on cball 0 (R(f 0));
@@ -788,7 +788,7 @@
-subsubsection\<open>Montel's theorem\<close>
+subsubsection%important\<open>Montel's theorem\<close>
text\<open>a sequence of holomorphic functions uniformly bounded
on compact subsets of an open set S has a subsequence that converges to a
--- a/src/HOL/Analysis/Homeomorphism.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Homeomorphism.thy Tue Jan 22 22:57:16 2019 +0000
@@ -2,7 +2,7 @@
Author: LC Paulson (ported from HOL Light)
*)
-section%important \<open>Homeomorphism Theorems\<close>
+section \<open>Homeomorphism Theorems\<close>
theory Homeomorphism
imports Homotopy
--- a/src/HOL/Analysis/Improper_Integral.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Improper_Integral.thy Tue Jan 22 22:57:16 2019 +0000
@@ -1,4 +1,4 @@
-section%important \<open>Continuity of the indefinite integral; improper integral theorem\<close>
+section \<open>Continuity of the indefinite integral; improper integral theorem\<close>
theory "Improper_Integral"
imports Equivalence_Lebesgue_Henstock_Integration
--- a/src/HOL/Analysis/Tagged_Division.thy Tue Jan 22 21:16:48 2019 +0000
+++ b/src/HOL/Analysis/Tagged_Division.thy Tue Jan 22 22:57:16 2019 +0000
@@ -2301,7 +2301,7 @@
with ptag that show ?thesis by auto
qed
-subsubsection \<open>Covering lemma\<close>
+subsubsection%important \<open>Covering lemma\<close>
text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's