# HG changeset patch # User Angeliki KoutsoukouArgyraki # Date 1548197836 0 # Node ID b5163b2132c583a5f55d09f6b5919e7be79a27d3 # Parent ce36bed06dee281efeb20e0124a7630deea7f8ab minor tagging updates in 13 theories diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Binary_Product_Measure.thy --- 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 \Binary Product Measure\ +section \Binary Product Measure\ theory Binary_Product_Measure imports Nonnegative_Lebesgue_Integration diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Bochner_Integration.thy --- 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 \Bochner Integration for Vector-Valued Functions\ +section \Bochner Integration for Vector-Valued Functions\ theory Bochner_Integration imports Finite_Product_Measure diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Borel_Space.thy --- 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 \Borel Space\ +section \Borel Space\ 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 \ B | A B. open A \ open B}" +proposition open_prod_generated: "open = generate_topology {A \ B | A B. open A \ open B}" proof - have "{A \ B :: ('a \ 'b) set | A B. open A \ open B} = ((\(a, b). a \ b) ` ({A. open A} \ {A. open A}))" by auto @@ -509,7 +509,7 @@ shows "borel = sigma UNIV (range (\(i, j). F i j))" using assms by (intro borel_eq_sigmaI1[where X="range G" and F="(\(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 \ 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" diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Caratheodory.thy --- 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 \Caratheodory Extension Theorem\ +section \Caratheodory Extension Theorem\ theory Caratheodory imports Measure_Space @@ -54,7 +54,7 @@ definition%important outer_measure_space where "outer_measure_space M f \ positive M f \ increasing M f \ countably_subadditive M f" -subsubsection \Lambda Systems\ +subsubsection%important \Lambda Systems\ definition%important lambda_system :: "'a set \ 'a set set \ ('a set \ ennreal) \ 'a set set" where @@ -635,7 +635,7 @@ qed qed -subsubsection \Caratheodory on semirings\ +subsubsection%important \Caratheodory on semirings\ theorem (in semiring_of_sets) caratheodory: assumes pos: "positive M \" and ca: "countably_additive M \" diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Extended_Real_Limits.thy --- 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 \Limits on the Extended Real Number Line\ (* TO FIX: perhaps put all Nonstandard Analysis related +section \Limits on the Extended Real Number Line\ (* TO FIX: perhaps put all Nonstandard Analysis related topics together? *) theory Extended_Real_Limits @@ -391,7 +391,7 @@ qed -subsubsection \Continuity of addition\ +subsubsection%important \Continuity of addition\ text \The next few lemmas remove an unnecessary assumption in \tendsto_add_ereal\, culminating in \tendsto_add_ereal_general\ 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 \Continuity of multiplication\ +subsubsection%important \Continuity of multiplication\ text \In the same way as for addition, we prove that the multiplication is continuous on ereal times ereal, except at \(\, 0)\ and \(-\, 0)\ and \(0, \)\ and \(0, -\)\, @@ -659,7 +659,7 @@ by (cases "c = 0", auto simp add: assms tendsto_mult_ereal) -subsubsection \Continuity of division\ +subsubsection%important \Continuity of division\ lemma tendsto_inverse_ereal_PInf: fixes u::"_ \ ereal" diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Fashoda_Theorem.thy --- 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 \Fashoda Meet Theorem\ +section \Fashoda Meet Theorem\ theory Fashoda_Theorem imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Finite_Product_Measure.thy --- 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 \Finite Product Measure\ +section \Finite Product Measure\ theory Finite_Product_Measure imports Binary_Product_Measure diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Function_Topology.thy --- 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 \Product Topology\ +section \Product Topology\ (* FIX see comments by the author *) text \We want to define the product topology. @@ -63,7 +63,7 @@ subsection \Topology without type classes\ -subsubsection \The topology generated by some (open) subsets\ +subsubsection%important \The topology generated by some (open) subsets\ text \In the definition below of a generated topology, the \Empty\ case is not necessary, as it follows from \UN\ taking for \K\ the empty set. However, it is convenient to have, @@ -257,7 +257,7 @@ qed qed -subsubsection \Continuity\ +subsubsection%important \Continuity\ text \We will need to deal with continuous maps in terms of topologies and not in terms of type classes, as defined below.\ @@ -335,7 +335,7 @@ using assms unfolding continuous_on_topo_def by auto -subsubsection \Pullback topology\ +subsubsection%important \Pullback topology\ text \Pulling back a topology by map gives again a topology. \subtopology\ is a special case of this notion, pulling back by the identity. We introduce the general notion as @@ -808,7 +808,7 @@ qed -subsubsection \Powers of a single topological space as a topological space, using type classes\ +subsubsection%important \Powers of a single topological space as a topological space, using type classes\ instantiation "fun" :: (type, topological_space) topological_space begin @@ -884,7 +884,7 @@ "continuous_on UNIV f \ (\i. continuous_on UNIV (\x. f x i))" by (auto intro: continuous_on_product_then_coordinatewise) -subsubsection \Topological countability for product spaces\ +subsubsection%important \Topological countability for product spaces\ text \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 diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Further_Topology.thy --- 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 \Extending Continous Maps, Invariance of Domain, etc\ (*FIX rename? *) +section \Extending Continous Maps, Invariance of Domain, etc\ (*FIX rename? *) text\Ported from HOL Light (moretop.ml) by L C Paulson\ diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Great_Picard.thy --- 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 \The Great Picard Theorem and its Applications\ +section \The Great Picard Theorem and its Applications\ text\Ported from HOL Light (cauchy.ml) by L C Paulson, 2017\ @@ -376,7 +376,7 @@ subsection\The Little Picard Theorem\ -proposition Landau_Picard: +theorem Landau_Picard: obtains R where "\z. 0 < R z" "\f. \f holomorphic_on cball 0 (R(f 0)); @@ -788,7 +788,7 @@ -subsubsection\Montel's theorem\ +subsubsection%important\Montel's theorem\ text\a sequence of holomorphic functions uniformly bounded on compact subsets of an open set S has a subsequence that converges to a diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Homeomorphism.thy --- 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 \Homeomorphism Theorems\ +section \Homeomorphism Theorems\ theory Homeomorphism imports Homotopy diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Improper_Integral.thy --- 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 \Continuity of the indefinite integral; improper integral theorem\ +section \Continuity of the indefinite integral; improper integral theorem\ theory "Improper_Integral" imports Equivalence_Lebesgue_Henstock_Integration diff -r ce36bed06dee -r b5163b2132c5 src/HOL/Analysis/Tagged_Division.thy --- 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 \Covering lemma\ +subsubsection%important \Covering lemma\ text\ 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