--- a/src/HOL/Analysis/Arcwise_Connected.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Mon Apr 09 16:20:23 2018 +0200
@@ -109,7 +109,7 @@
subsection\<open>Arcwise Connections\<close>
-subsection\<open>Density of points with dyadic rational coordinates.\<close>
+subsection\<open>Density of points with dyadic rational coordinates\<close>
proposition closure_dyadic_rationals:
"closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Apr 09 16:20:23 2018 +0200
@@ -16,7 +16,7 @@
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
-section \<open>Results connected with topological dimension.\<close>
+section \<open>Results connected with topological dimension\<close>
theory Brouwer_Fixpoint
imports Path_Connected Homeomorphism
@@ -117,7 +117,7 @@
qed
-subsection \<open>The key "counting" observation, somewhat abstracted.\<close>
+subsection \<open>The key "counting" observation, somewhat abstracted\<close>
lemma kuhn_counting_lemma:
fixes bnd compo compo' face S F
@@ -148,7 +148,7 @@
by auto
qed
-subsection \<open>The odd/even result for faces of complete vertices, generalized.\<close>
+subsection \<open>The odd/even result for faces of complete vertices, generalized\<close>
lemma kuhn_complete_lemma:
assumes [simp]: "finite simplices"
@@ -2367,7 +2367,7 @@
qed
-subsection\<open>Punctured affine hulls, etc.\<close>
+subsection\<open>Punctured affine hulls, etc\<close>
lemma continuous_on_compact_surface_projection_aux:
fixes S :: "'a::t2_space set"
@@ -2716,7 +2716,7 @@
by blast
qed
-subsection\<open>Absolute retracts, Etc.\<close>
+subsection\<open>Absolute retracts, etc\<close>
text\<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also
Euclidean neighbourhood retracts (ENR). We define AR and ANR by
@@ -3110,7 +3110,7 @@
shows "S homeomorphic T \<Longrightarrow> ANR S \<longleftrightarrow> ANR T"
by (metis ANR_homeomorphic_ANR homeomorphic_sym)
-subsection\<open> Analogous properties of ENRs.\<close>
+subsection\<open> Analogous properties of ENRs\<close>
proposition ENR_imp_absolute_neighbourhood_retract:
fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
@@ -4274,7 +4274,7 @@
shows "ANR c"
by (metis ANR_connected_component_ANR assms componentsE)
-subsection\<open>Original ANR material, now for ENRs.\<close>
+subsection\<open>Original ANR material, now for ENRs\<close>
lemma ENR_bounded:
fixes S :: "'a::euclidean_space set"
@@ -4438,7 +4438,7 @@
by (simp add: ENR_imp_ANR ENR_sphere)
-subsection\<open>Spheres are connected, etc.\<close>
+subsection\<open>Spheres are connected, etc\<close>
lemma locally_path_connected_sphere_gen:
fixes S :: "'a::euclidean_space set"
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Mon Apr 09 16:20:23 2018 +0200
@@ -1,4 +1,4 @@
-section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
+section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\<close>
theory Cartesian_Euclidean_Space
imports Finite_Cartesian_Product Derivative
@@ -21,7 +21,7 @@
qed simp
qed simp
-subsection\<open>Basic componentwise operations on vectors.\<close>
+subsection\<open>Basic componentwise operations on vectors\<close>
instantiation vec :: (times, finite) times
begin
@@ -93,7 +93,7 @@
where "c *s x = (\<chi> i. c * (x$i))"
-subsection \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space.\<close>
+subsection \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\<close>
lemma sum_cong_aux:
"(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> sum f A = sum g A"
@@ -170,7 +170,7 @@
vector_scaleR_component cond_component
-subsection \<open>Some frequently useful arithmetic lemmas over vectors.\<close>
+subsection \<open>Some frequently useful arithmetic lemmas over vectors\<close>
instance vec :: (semigroup_mult, finite) semigroup_mult
by standard (vector mult.assoc)
@@ -719,7 +719,7 @@
done
-subsection\<open>Some bounds on components etc. relative to operator norm.\<close>
+subsection\<open>Some bounds on components etc. relative to operator norm\<close>
lemma norm_column_le_onorm:
fixes A :: "real^'n^'m"
@@ -1416,7 +1416,7 @@
subsection \<open>Component of the differential must be zero if it exists at a local
- maximum or minimum for that corresponding component.\<close>
+ maximum or minimum for that corresponding component\<close>
lemma differential_zero_maxmin_cart:
fixes f::"real^'a \<Rightarrow> real^'b"
@@ -1489,7 +1489,7 @@
end
-subsection\<open>The collapse of the general concepts to dimension one.\<close>
+subsection\<open>The collapse of the general concepts to dimension one\<close>
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
by (simp add: vec_eq_iff)
@@ -1510,7 +1510,7 @@
by (auto simp add: norm_real dist_norm)
-subsection\<open>Explicit vector construction from lists.\<close>
+subsection\<open>Explicit vector construction from lists\<close>
definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Apr 09 16:20:23 2018 +0200
@@ -3550,7 +3550,7 @@
apply (force simp: algebra_simps)
done
-subsubsection\<open>Some lemmas about negating a path.\<close>
+subsubsection\<open>Some lemmas about negating a path\<close>
lemma valid_path_negatepath: "valid_path \<gamma> \<Longrightarrow> valid_path (uminus \<circ> \<gamma>)"
unfolding o_def using piecewise_C1_differentiable_neg valid_path_def by blast
@@ -3965,7 +3965,7 @@
qed
-subsection\<open>Continuity of winding number and invariance on connected sets.\<close>
+subsection\<open>Continuity of winding number and invariance on connected sets\<close>
lemma continuous_at_winding_number:
fixes z::complex
@@ -4436,7 +4436,7 @@
qed
-subsection\<open>Cauchy's integral formula, again for a convex enclosing set.\<close>
+subsection\<open>Cauchy's integral formula, again for a convex enclosing set\<close>
lemma Cauchy_integral_formula_weak:
assumes s: "convex s" and "finite k" and conf: "continuous_on s f"
@@ -5374,7 +5374,7 @@
using assms by (auto simp: vector_derivative_circlepath norm_mult intro!: contour_integral_uniform_limit)
-subsection\<open> General stepping result for derivative formulas.\<close>
+subsection\<open> General stepping result for derivative formulas\<close>
proposition Cauchy_next_derivative:
assumes "continuous_on (path_image \<gamma>) f'"
@@ -5614,7 +5614,7 @@
by simp (rule fder)
qed
-subsection\<open> Existence of all higher derivatives.\<close>
+subsection\<open>Existence of all higher derivatives\<close>
proposition derivative_is_holomorphic:
assumes "open s"
@@ -5699,7 +5699,7 @@
qed
-subsection\<open> Morera's theorem.\<close>
+subsection\<open>Morera's theorem\<close>
lemma Morera_local_triangle_ball:
assumes "\<And>z. z \<in> s
@@ -5783,7 +5783,7 @@
-subsection\<open> Combining theorems for higher derivatives including Leibniz rule.\<close>
+subsection\<open>Combining theorems for higher derivatives including Leibniz rule\<close>
lemma higher_deriv_linear [simp]:
"(deriv ^^ n) (\<lambda>w. c*w) = (\<lambda>z. if n = 0 then c*z else if n = 1 then c else 0)"
@@ -6139,7 +6139,7 @@
by (simp add: power2_eq_square)
-subsection\<open>A holomorphic function is analytic, i.e. has local power series.\<close>
+subsection\<open>A holomorphic function is analytic, i.e. has local power series\<close>
theorem holomorphic_power_series:
assumes holf: "f holomorphic_on ball z r"
@@ -6255,7 +6255,7 @@
qed
-subsection\<open>The Liouville theorem and the Fundamental Theorem of Algebra.\<close>
+subsection\<open>The Liouville theorem and the Fundamental Theorem of Algebra\<close>
text\<open> These weak Liouville versions don't even need the derivative formula.\<close>
@@ -6343,7 +6343,7 @@
qed
-subsection\<open> Weierstrass convergence theorem.\<close>
+subsection\<open>Weierstrass convergence theorem\<close>
proposition holomorphic_uniform_limit:
assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and> (f n) holomorphic_on ball z r) F"
@@ -6490,7 +6490,7 @@
qed
-subsection\<open>Some more simple/convenient versions for applications.\<close>
+subsection\<open>Some more simple/convenient versions for applications\<close>
lemma holomorphic_uniform_sequence:
assumes S: "open S"
@@ -6548,7 +6548,7 @@
qed
-subsection\<open>On analytic functions defined by a series.\<close>
+subsection\<open>On analytic functions defined by a series\<close>
lemma series_and_derivative_comparison:
fixes S :: "complex set"
@@ -6767,7 +6767,7 @@
by (simp add: analytic_on_open holomorphic_iff_power_series)
-subsection\<open>Equality between holomorphic functions, on open ball then connected set.\<close>
+subsection\<open>Equality between holomorphic functions, on open ball then connected set\<close>
lemma holomorphic_fun_eq_on_ball:
"\<lbrakk>f holomorphic_on ball z r; g holomorphic_on ball z r;
@@ -6846,7 +6846,7 @@
done
-subsection\<open>Some basic lemmas about poles/singularities.\<close>
+subsection\<open>Some basic lemmas about poles/singularities\<close>
lemma pole_lemma:
assumes holf: "f holomorphic_on s" and a: "a \<in> interior s"
@@ -7002,7 +7002,7 @@
qed
-subsection\<open>General, homology form of Cauchy's theorem.\<close>
+subsection\<open>General, homology form of Cauchy's theorem\<close>
text\<open>Proof is based on Dixon's, as presented in Lang's "Complex Analysis" book (page 147).\<close>
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Mon Apr 09 16:20:23 2018 +0200
@@ -174,7 +174,7 @@
"(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
by (metis DERIV_zero_unique UNIV_I convex_UNIV)
-subsection \<open>Some limit theorems about real part of real series etc.\<close>
+subsection \<open>Some limit theorems about real part of real series etc\<close>
(*MOVE? But not to Finite_Cartesian_Product*)
lemma sums_vec_nth :
--- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Apr 09 16:20:23 2018 +0200
@@ -77,7 +77,7 @@
"f holomorphic_on s \<Longrightarrow> (\<lambda>x. exp (f x)) holomorphic_on s"
using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def)
-subsection\<open>Euler and de Moivre formulas.\<close>
+subsection\<open>Euler and de Moivre formulas\<close>
text\<open>The sine series times @{term i}\<close>
lemma sin_i_eq: "(\<lambda>n. (\<i> * sin_coeff n) * z^n) sums (\<i> * sin z)"
@@ -176,7 +176,7 @@
lemma holomorphic_on_cos: "cos holomorphic_on s"
by (simp add: field_differentiable_within_cos holomorphic_on_def)
-subsection\<open>Get a nice real/imaginary separation in Euler's formula.\<close>
+subsection\<open>Get a nice real/imaginary separation in Euler's formula\<close>
lemma Euler: "exp(z) = of_real(exp(Re z)) *
(of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
@@ -626,7 +626,7 @@
qed
-subsection\<open>Taylor series for complex exponential, sine and cosine.\<close>
+subsection\<open>Taylor series for complex exponential, sine and cosine\<close>
declare power_Suc [simp del]
@@ -3503,7 +3503,7 @@
lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
-subsection\<open>Some interrelationships among the real inverse trig functions.\<close>
+subsection\<open>Some interrelationships among the real inverse trig functions\<close>
lemma arccos_arctan:
assumes "-1 < x" "x < 1"
@@ -3573,7 +3573,7 @@
using arccos_arcsin_sqrt_pos [of "-x"]
by (simp add: arccos_minus)
-subsection\<open>continuity results for arcsin and arccos.\<close>
+subsection\<open>Continuity results for arcsin and arccos\<close>
lemma continuous_on_Arcsin_real [continuous_intros]:
"continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
--- a/src/HOL/Analysis/Conformal_Mappings.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Mon Apr 09 16:20:23 2018 +0200
@@ -1,4 +1,4 @@
-section \<open>Conformal Mappings. Consequences of Cauchy's integral theorem.\<close>
+section \<open>Conformal Mappings and Consequences of Cauchy's integral theorem\<close>
text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2016)\<close>
--- a/src/HOL/Analysis/Connected.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Connected.thy Mon Apr 09 16:20:23 2018 +0200
@@ -2,13 +2,13 @@
Material split off from Topology_Euclidean_Space
*)
-section \<open>Connected Components, Homeomorphisms, Baire property, etc.\<close>
+section \<open>Connected Components, Homeomorphisms, Baire property, etc\<close>
theory Connected
imports Topology_Euclidean_Space
begin
-subsection%unimportant \<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)
@@ -961,7 +961,7 @@
qed
qed
-subsection%unimportant \<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%unimportant\<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"
@@ -1515,7 +1515,7 @@
by (simp add: compact_eq_bounded_closed)
qed
-subsection%unimportant \<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"
@@ -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%unimportant \<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"
@@ -2363,7 +2363,7 @@
unfolding mem_interior using \<open>e > 0\<close> by auto
qed
-subsection \<open>Continuity implies uniform continuity on a compact domain.\<close>
+subsection \<open>Continuity implies uniform continuity on a compact domain\<close>
text\<open>From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of
J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)\<close>
@@ -2666,7 +2666,7 @@
qed
-subsection \<open>The diameter of a set.\<close>
+subsection \<open>The diameter of a set\<close>
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)"
@@ -3014,7 +3014,7 @@
qed
-subsection%unimportant \<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"
@@ -3321,7 +3321,7 @@
using assms
by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified])
-subsubsection\<open>Some more convenient intermediate-value theorem formulations.\<close>
+subsubsection\<open>Some more convenient intermediate-value theorem formulations\<close>
lemma connected_ivt_hyperplane:
assumes "connected S" and xy: "x \<in> S" "y \<in> S" and b: "inner a x \<le> b" "b \<le> inner a y"
@@ -3901,7 +3901,7 @@
qed
-subsection \<open>"Isometry" (up to constant bounds) of injective linear map etc.\<close>
+subsection \<open>"Isometry" (up to constant bounds) of injective linear map etc\<close>
lemma cauchy_isometric:
assumes e: "e > 0"
@@ -4976,7 +4976,7 @@
-subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4).\<close>
+subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4)\<close>
lemma connected_Un_clopen_in_complement:
--- a/src/HOL/Analysis/Continuous_Extension.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Continuous_Extension.thy Mon Apr 09 16:20:23 2018 +0200
@@ -295,7 +295,7 @@
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>
+subsection\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
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>
--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy Mon Apr 09 16:20:23 2018 +0200
@@ -3,7 +3,7 @@
Author: Johannes Hölzl, TU München
*)
-section \<open>Non-denumerability of the Continuum.\<close>
+section \<open>Non-denumerability of the Continuum\<close>
theory Continuum_Not_Denumerable
imports
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Apr 09 16:20:23 2018 +0200
@@ -4283,7 +4283,7 @@
by (metis low_dim_interior)
-subsection \<open>Caratheodory's theorem.\<close>
+subsection \<open>Caratheodory's theorem\<close>
lemma convex_hull_caratheodory_aff_dim:
fixes p :: "('a::euclidean_space) set"
@@ -5151,7 +5151,7 @@
by (metis Int_absorb1 Int_absorb2 convex_hull_subset_affine_hull hull_hull hull_mono hull_subset)
-subsection%unimportant \<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%unimportant \<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"
@@ -5621,7 +5621,7 @@
by(cases "s = {}") auto
-subsection \<open>Closest point of a convex set is unique, with a continuous projection.\<close>
+subsection \<open>Closest point of a convex set is unique, with a continuous projection\<close>
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))"
@@ -5811,7 +5811,7 @@
qed
-subsubsection%unimportant \<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}"
@@ -6132,7 +6132,7 @@
using hull_subset[of s convex] convex_hull_empty by auto
-subsection%unimportant \<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"
@@ -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%unimportant \<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
--- a/src/HOL/Analysis/Derivative.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy Mon Apr 09 16:20:23 2018 +0200
@@ -15,7 +15,7 @@
subsection \<open>Derivatives\<close>
-subsubsection \<open>Combining theorems.\<close>
+subsubsection \<open>Combining theorems\<close>
lemmas has_derivative_id = has_derivative_ident
lemmas has_derivative_neg = has_derivative_minus
@@ -32,7 +32,7 @@
by (intro derivative_eq_intros) auto
-subsection \<open>Derivative with composed bilinear function.\<close>
+subsection \<open>Derivative with composed bilinear function\<close>
lemma has_derivative_bilinear_within:
assumes "(f has_derivative f') (at x within s)"
--- a/src/HOL/Analysis/Determinants.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Determinants.thy Mon Apr 09 16:20:23 2018 +0200
@@ -929,7 +929,7 @@
by auto
qed
-subsection \<open>Orthogonality of a transformation and matrix.\<close>
+subsection \<open>Orthogonality of a transformation and matrix\<close>
definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
@@ -1087,7 +1087,7 @@
using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
-subsection \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
+subsection \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
lemma scaling_linear:
fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
@@ -1157,7 +1157,7 @@
by (auto simp: orthogonal_transformation_isometry)
qed
-subsection\<open> We can find an orthogonal matrix taking any unit vector to any other.\<close>
+subsection\<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
lemma orthogonal_matrix_transpose [simp]:
"orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
@@ -1251,7 +1251,7 @@
qed
-subsection \<open>Can extend an isometry from unit sphere.\<close>
+subsection \<open>Can extend an isometry from unit sphere\<close>
lemma isometry_sphere_extend:
fixes f:: "'a::real_inner \<Rightarrow> 'a"
@@ -1349,7 +1349,7 @@
done
qed
-subsection \<open>Rotation, reflection, rotoinversion.\<close>
+subsection \<open>Rotation, reflection, rotoinversion\<close>
definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
--- a/src/HOL/Analysis/Fashoda_Theorem.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Mon Apr 09 16:20:23 2018 +0200
@@ -8,7 +8,7 @@
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
begin
-subsection \<open>Bijections between intervals.\<close>
+subsection \<open>Bijections between intervals\<close>
definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
where "interval_bij =
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Mon Apr 09 16:20:23 2018 +0200
@@ -2,7 +2,7 @@
Author: Amine Chaieb, University of Cambridge
*)
-section \<open>Definition of finite Cartesian product types.\<close>
+section \<open>Definition of finite Cartesian product types\<close>
theory Finite_Cartesian_Product
imports
@@ -13,7 +13,7 @@
"HOL-Library.FuncSet"
begin
-subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>
+subsection \<open>Finite Cartesian products, with indexing and lambdas\<close>
typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set"
morphisms vec_nth vec_lambda ..
--- a/src/HOL/Analysis/Further_Topology.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Mon Apr 09 16:20:23 2018 +0200
@@ -1,4 +1,4 @@
-section \<open>Extending Continous Maps, Invariance of Domain, etc..\<close>
+section \<open>Extending Continous Maps, Invariance of Domain, etc\<close>
text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
@@ -367,7 +367,7 @@
-subsection\<open> Some technical lemmas about extending maps from cell complexes.\<close>
+subsection\<open> Some technical lemmas about extending maps from cell complexes\<close>
lemma extending_maps_Union_aux:
assumes fin: "finite \<F>"
@@ -981,7 +981,7 @@
-subsection\<open> Special cases and corollaries involving spheres.\<close>
+subsection\<open> Special cases and corollaries involving spheres\<close>
lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
by (auto simp: disjnt_def)
@@ -2727,7 +2727,7 @@
using clopen [of S] False by simp
qed
-subsection\<open> Dimension-based conditions for various homeomorphisms.\<close>
+subsection\<open>Dimension-based conditions for various homeomorphisms\<close>
lemma homeomorphic_subspaces_eq:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
@@ -3896,7 +3896,7 @@
qed
-subsection\<open>Another simple case where sphere maps are nullhomotopic.\<close>
+subsection\<open>Another simple case where sphere maps are nullhomotopic\<close>
lemma inessential_spheremap_2_aux:
fixes f :: "'a::euclidean_space \<Rightarrow> complex"
@@ -3962,7 +3962,7 @@
qed
-subsection\<open>Holomorphic logarithms and square roots.\<close>
+subsection\<open>Holomorphic logarithms and square roots\<close>
lemma contractible_imp_holomorphic_log:
assumes holf: "f holomorphic_on S"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Apr 09 16:20:23 2018 +0200
@@ -3,7 +3,7 @@
Huge cleanup by LCP
*)
-section \<open>Henstock-Kurzweil gauge integration in many dimensions.\<close>
+section \<open>Henstock-Kurzweil gauge integration in many dimensions\<close>
theory Henstock_Kurzweil_Integration
imports
@@ -28,7 +28,7 @@
by blast
(* END MOVE *)
-subsection \<open>Content (length, area, volume...) of an interval.\<close>
+subsection \<open>Content (length, area, volume...) of an interval\<close>
abbreviation content :: "'a::euclidean_space set \<Rightarrow> real"
where "content s \<equiv> measure lborel s"
@@ -313,7 +313,7 @@
lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
by auto
-subsection \<open>Basic theorems about integrals.\<close>
+subsection \<open>Basic theorems about integrals\<close>
lemma has_integral_eq_rhs: "(f has_integral j) S \<Longrightarrow> i = j \<Longrightarrow> (f has_integral i) S"
by (rule forw_subst)
@@ -909,7 +909,7 @@
-subsection \<open>Cauchy-type criterion for integrability.\<close>
+subsection \<open>Cauchy-type criterion for integrability\<close>
proposition integrable_Cauchy:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::{real_normed_vector,complete_space}"
@@ -1012,7 +1012,7 @@
qed
-subsection \<open>Additivity of integral on abutting intervals.\<close>
+subsection \<open>Additivity of integral on abutting intervals\<close>
lemma tagged_division_split_left_inj_content:
assumes \<D>: "\<D> tagged_division_of S"
@@ -1261,7 +1261,7 @@
qed
-subsection \<open>A sort of converse, integrability on subintervals.\<close>
+subsection \<open>A sort of converse, integrability on subintervals\<close>
lemma has_integral_separate_sides:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -1459,7 +1459,7 @@
qed
qed
-subsection \<open>Bounds on the norm of Riemann sums and the integral itself.\<close>
+subsection \<open>Bounds on the norm of Riemann sums and the integral itself\<close>
lemma dsum_bound:
assumes "p division_of (cbox a b)"
@@ -1562,7 +1562,7 @@
by (metis integrable_integral has_integral_bound assms)
-subsection \<open>Similar theorems about relationship among components.\<close>
+subsection \<open>Similar theorems about relationship among components\<close>
lemma rsum_component_le:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -1764,7 +1764,7 @@
using assms
by (metis box_real(2) integral_component_ubound)
-subsection \<open>Uniform limit of integrable functions is integrable.\<close>
+subsection \<open>Uniform limit of integrable functions is integrable\<close>
lemma real_arch_invD:
"0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
@@ -1907,13 +1907,13 @@
lemmas integrable_uniform_limit_real = integrable_uniform_limit [where 'a=real, simplified]
-subsection \<open>Negligible sets.\<close>
+subsection \<open>Negligible sets\<close>
definition "negligible (s:: 'a::euclidean_space set) \<longleftrightarrow>
(\<forall>a b. ((indicator s :: 'a\<Rightarrow>real) has_integral 0) (cbox a b))"
-subsubsection \<open>Negligibility of hyperplane.\<close>
+subsubsection \<open>Negligibility of hyperplane\<close>
lemma content_doublesplit:
fixes a :: "'a::euclidean_space"
@@ -2082,7 +2082,7 @@
qed
-subsubsection \<open>Hence the main theorem about negligible sets.\<close>
+subsubsection \<open>Hence the main theorem about negligible sets\<close>
lemma has_integral_negligible_cbox:
@@ -2276,7 +2276,7 @@
by (auto simp: integral_def integrable_on_def)
-subsection \<open>Some other trivialities about negligible sets.\<close>
+subsection \<open>Some other trivialities about negligible sets\<close>
lemma negligible_subset:
assumes "negligible s" "t \<subseteq> s"
@@ -2366,7 +2366,7 @@
qed auto
-subsection \<open>Finite case of the spike theorem is quite commonly needed.\<close>
+subsection \<open>Finite case of the spike theorem is quite commonly needed\<close>
lemma has_integral_spike_finite:
assumes "finite S"
@@ -2414,7 +2414,7 @@
by (metis assms box_real(2) has_integral_bound_spike_finite)
-subsection \<open>In particular, the boundary of an interval is negligible.\<close>
+subsection \<open>In particular, the boundary of an interval is negligible\<close>
lemma negligible_frontier_interval: "negligible(cbox (a::'a::euclidean_space) b - box a b)"
proof -
@@ -2445,7 +2445,7 @@
using assms has_integral_spike_interior_eq by blast
-subsection \<open>Integrability of continuous functions.\<close>
+subsection \<open>Integrability of continuous functions\<close>
lemma operative_approximableI:
fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
@@ -2573,10 +2573,10 @@
by (auto intro!: integrable_continuous_interval simp: closed_segment_eq_real_ivl)
-subsection \<open>Specialization of additivity to one dimension.\<close>
-
-
-subsection \<open>A useful lemma allowing us to factor out the content size.\<close>
+subsection \<open>Specialization of additivity to one dimension\<close>
+
+
+subsection \<open>A useful lemma allowing us to factor out the content size\<close>
lemma has_integral_factor_content:
"(f has_integral i) (cbox a b) \<longleftrightarrow>
@@ -2642,7 +2642,7 @@
by (rule has_integral_factor_content)
-subsection \<open>Fundamental theorem of calculus.\<close>
+subsection \<open>Fundamental theorem of calculus\<close>
lemma interval_bounds_real:
fixes q b :: real
@@ -2884,7 +2884,7 @@
qed
-subsection \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
+subsection \<open>Only need trivial subintervals if the interval itself is trivial\<close>
proposition division_of_nontrivial:
fixes \<D> :: "'a::euclidean_space set set"
@@ -2970,7 +2970,7 @@
qed
-subsection \<open>Integrability on subintervals.\<close>
+subsection \<open>Integrability on subintervals\<close>
lemma operative_integrableI:
fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
@@ -3016,7 +3016,7 @@
shows "f integrable_on {c..d}"
by (metis assms box_real(2) integrable_subinterval)
-subsection \<open>Combining adjacent intervals in 1 dimension.\<close>
+subsection \<open>Combining adjacent intervals in 1 dimension\<close>
lemma has_integral_combine:
fixes a b c :: real and j :: "'a::banach"
@@ -3087,7 +3087,7 @@
using integral_combine[of b a c f] integral_combine[of a b c f]
by (auto simp: algebra_simps min_def)
-subsection \<open>Reduce integrability to "local" integrability.\<close>
+subsection \<open>Reduce integrability to "local" integrability\<close>
lemma integrable_on_little_subintervals:
fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
@@ -3116,7 +3116,7 @@
qed
-subsection \<open>Second FTC or existence of antiderivative.\<close>
+subsection \<open>Second FTC or existence of antiderivative\<close>
lemma integrable_const[intro]: "(\<lambda>x. c) integrable_on cbox a b"
unfolding integrable_on_def by blast
@@ -3204,7 +3204,7 @@
obtains g where "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
using integral_has_vector_derivative[OF assms] by auto
-subsection \<open>Combined fundamental theorem of calculus.\<close>
+subsection \<open>Combined fundamental theorem of calculus\<close>
lemma antiderivative_integral_continuous:
fixes f :: "real \<Rightarrow> 'a::banach"
@@ -3227,7 +3227,7 @@
qed
-subsection \<open>General "twiddling" for interval-to-interval function image.\<close>
+subsection \<open>General "twiddling" for interval-to-interval function image\<close>
lemma has_integral_twiddle:
assumes "0 < r"
@@ -3334,7 +3334,7 @@
qed
-subsection \<open>Special case of a basic affine transformation.\<close>
+subsection \<open>Special case of a basic affine transformation\<close>
lemma AE_lborel_inner_neq:
assumes k: "k \<in> Basis"
@@ -3460,7 +3460,7 @@
lemmas has_integral_affinity01 = has_integral_affinity [of _ _ 0 "1::real", simplified]
-subsection \<open>Special case of stretching coordinate axes separately.\<close>
+subsection \<open>Special case of stretching coordinate axes separately\<close>
lemma has_integral_stretch:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -3485,7 +3485,7 @@
by (force dest: has_integral_stretch)
-subsection \<open>even more special cases.\<close>
+subsection \<open>even more special cases\<close>
lemma uminus_interval_vector[simp]:
fixes a b :: "'a::euclidean_space"
@@ -3528,7 +3528,7 @@
by (rule integral_reflect)
-subsection \<open>Stronger form of FCT; quite a tedious proof.\<close>
+subsection \<open>Stronger form of FCT; quite a tedious proof\<close>
lemma split_minus[simp]: "(\<lambda>(x, k). f x k) x - (\<lambda>(x, k). g x k) x = (\<lambda>(x, k). f x k - g x k) x"
by (simp add: split_def)
@@ -3904,7 +3904,7 @@
qed
-subsection \<open>Stronger form with finite number of exceptional points.\<close>
+subsection \<open>Stronger form with finite number of exceptional points\<close>
lemma fundamental_theorem_of_calculus_interior_strong:
fixes f :: "real \<Rightarrow> 'a::banach"
@@ -4217,7 +4217,7 @@
by (auto simp: has_field_derivative_iff_has_vector_derivative)
-subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
+subsection \<open>This doesn't directly involve integration, but that gives an easy proof\<close>
lemma has_derivative_zero_unique_strong_interval:
fixes f :: "real \<Rightarrow> 'a::banach"
@@ -4251,7 +4251,7 @@
qed
-subsection \<open>Generalize a bit to any convex set.\<close>
+subsection \<open>Generalize a bit to any convex set\<close>
lemma has_derivative_zero_unique_strong_convex:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
@@ -4919,7 +4919,7 @@
qed
-subsection \<open>Continuity of the integral (for a 1-dimensional interval).\<close>
+subsection \<open>Continuity of the integral (for a 1-dimensional interval)\<close>
lemma integrable_alt:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
--- a/src/HOL/Analysis/Jordan_Curve.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy Mon Apr 09 16:20:23 2018 +0200
@@ -9,7 +9,7 @@
begin
-subsection\<open>Janiszewski's theorem.\<close>
+subsection\<open>Janiszewski's theorem\<close>
lemma Janiszewski_weak:
fixes a b::complex
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Mon Apr 09 16:20:23 2018 +0200
@@ -978,7 +978,8 @@
then show ?thesis
by (auto dest!: AE_not_in)
qed
-subsection\<open> A nice lemma for negligibility proofs.\<close>
+
+subsection \<open>A nice lemma for negligibility proofs\<close>
lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top"
by (metis summable_suminf_not_top)
--- a/src/HOL/Analysis/Path_Connected.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Mon Apr 09 16:20:23 2018 +0200
@@ -3380,7 +3380,7 @@
by (metis dw_le norm_minus_commute not_less order_trans rle wy)
qed
-section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps.\<close>
+section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps\<close>
text%important\<open> We often just want to require that it fixes some subset, but to take in
the case of a loop homotopy, it's convenient to have a general property P.\<close>
@@ -3487,7 +3487,7 @@
qed
-subsection%unimportant\<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
@@ -3742,7 +3742,7 @@
qed
-subsection\<open>Homotopy of paths, maintaining the same endpoints.\<close>
+subsection\<open>Homotopy of paths, maintaining the same endpoints\<close>
definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
@@ -3958,7 +3958,7 @@
using%unimportant homotopic_paths_rinv [of "reversepath p" s] assms by simp
-subsection\<open> Homotopy of loops without requiring preservation of endpoints.\<close>
+subsection\<open>Homotopy of loops without requiring preservation of endpoints\<close>
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>
@@ -4197,7 +4197,7 @@
qed
-subsection%unimportant\<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"
@@ -5521,7 +5521,7 @@
by (metis open_openin openin_topspace subtopology_superset top.extremum topspace_euclidean_subtopology)
qed
-subsection\<open>Sura-Bura's results about compact components of sets.\<close>
+subsection\<open>Sura-Bura's results about compact components of sets\<close>
proposition Sura_Bura_compact:
fixes S :: "'a::euclidean_space set"
@@ -7452,7 +7452,7 @@
-subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
+subsection\<open>Self-homeomorphisms shuffling points about in various ways\<close>
subsubsection%unimportant\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
--- a/src/HOL/Analysis/Poly_Roots.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Poly_Roots.thy Mon Apr 09 16:20:23 2018 +0200
@@ -8,7 +8,7 @@
imports Complex_Main
begin
-subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
+subsection\<open>Basics about polynomial functions: extremal behaviour and root counts\<close>
lemma sub_polyfun:
fixes x :: "'a::{comm_ring,monoid_mult}"
--- a/src/HOL/Analysis/Polytope.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Polytope.thy Mon Apr 09 16:20:23 2018 +0200
@@ -1,4 +1,4 @@
-section \<open>Faces, Extreme Points, Polytopes, Polyhedra etc.\<close>
+section \<open>Faces, Extreme Points, Polytopes, Polyhedra etc\<close>
text\<open>Ported from HOL Light by L C Paulson\<close>
--- a/src/HOL/Analysis/Riemann_Mapping.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Mon Apr 09 16:20:23 2018 +0200
@@ -8,7 +8,7 @@
imports Great_Picard
begin
-subsection\<open>Moebius functions are biholomorphisms of the unit disc.\<close>
+subsection\<open>Moebius functions are biholomorphisms of the unit disc\<close>
definition Moebius_function :: "[real,complex,complex] \<Rightarrow> complex" where
"Moebius_function \<equiv> \<lambda>t w z. exp(\<i> * of_real t) * (z - w) / (1 - cnj w * z)"
@@ -853,7 +853,7 @@
using convex_imp_contractible homeomorphic_contractible_eq simply_connected_eq_homeomorphic_to_disc by auto
-subsection\<open>A further chain of equivalences about components of the complement of a simply connected set.\<close>
+subsection\<open>A further chain of equivalences about components of the complement of a simply connected set\<close>
text\<open>(following 1.35 in Burckel'S book)\<close>
--- a/src/HOL/Analysis/Starlike.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Starlike.thy Mon Apr 09 16:20:23 2018 +0200
@@ -6,7 +6,7 @@
Author: Johannes Hoelzl, TU Muenchen
*)
-section \<open>Line segments, Starlike Sets, etc.\<close>
+section \<open>Line segments, Starlike Sets, etc\<close>
theory Starlike
imports Convex_Euclidean_Space
@@ -4157,7 +4157,7 @@
by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
qed
-subsection%unimportant\<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"
@@ -7119,7 +7119,7 @@
done
qed
-subsection\<open>Decomposing a vector into parts in orthogonal subspaces.\<close>
+subsection\<open>Decomposing a vector into parts in orthogonal subspaces\<close>
text\<open>existence of orthonormal basis for a subspace.\<close>
@@ -7470,7 +7470,7 @@
finally show "dim T \<le> dim S" by simp
qed
-subsection\<open>Lower-dimensional affine subsets are nowhere dense.\<close>
+subsection\<open>Lower-dimensional affine subsets are nowhere dense\<close>
proposition%important dense_complement_subspace:
fixes S :: "'a :: euclidean_space set"
@@ -7583,7 +7583,7 @@
by (simp add: assms dense_complement_convex)
-subsection%unimportant\<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>
--- a/src/HOL/Analysis/Tagged_Division.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy Mon Apr 09 16:20:23 2018 +0200
@@ -55,7 +55,7 @@
by (simp add: field_simps)
qed
-subsection \<open>Some useful lemmas about intervals.\<close>
+subsection \<open>Some useful lemmas about intervals\<close>
lemma interior_subset_union_intervals:
assumes "i = cbox a b"
@@ -130,7 +130,7 @@
lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
by (simp add: box_ne_empty)
-subsection \<open>Bounds on intervals where they exist.\<close>
+subsection \<open>Bounds on intervals where they exist\<close>
definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
@@ -192,7 +192,7 @@
by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
qed
-subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
+subsection \<open>The notion of a gauge --- simply an open set containing the point\<close>
definition "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
@@ -242,14 +242,14 @@
"(\<forall>x. \<exists>d :: real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)"
by (metis zero_less_one)
-subsection \<open>Attempt a systematic general set of "offset" results for components.\<close>
+subsection \<open>Attempt a systematic general set of "offset" results for components\<close>
lemma gauge_modify:
assumes "(\<forall>S. open S \<longrightarrow> open {x. f(x) \<in> S})" "gauge d"
shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
using assms unfolding gauge_def by force
-subsection \<open>Divisions.\<close>
+subsection \<open>Divisions\<close>
definition division_of (infixl "division'_of" 40)
where
@@ -995,7 +995,7 @@
}
qed
-subsection \<open>Tagged (partial) divisions.\<close>
+subsection \<open>Tagged (partial) divisions\<close>
definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
where "s tagged_partial_division_of i \<longleftrightarrow>
@@ -1828,7 +1828,7 @@
qed
-subsection \<open>Special case of additivity we need for the FTC.\<close>
+subsection \<open>Special case of additivity we need for the FTC\<close>
lemma additive_tagged_division_1:
fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
@@ -1856,7 +1856,7 @@
qed
-subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
+subsection \<open>Fine-ness of a partition w.r.t. a gauge\<close>
definition fine (infixr "fine" 46)
where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
@@ -1887,7 +1887,7 @@
lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
unfolding fine_def by blast
-subsection \<open>Some basic combining lemmas.\<close>
+subsection \<open>Some basic combining lemmas\<close>
lemma tagged_division_Union_exists:
assumes "finite I"
@@ -1907,14 +1907,14 @@
qed
-subsection \<open>The set we're concerned with must be closed.\<close>
+subsection \<open>The set we're concerned with must be closed\<close>
lemma division_of_closed:
fixes i :: "'n::euclidean_space set"
shows "s division_of i \<Longrightarrow> closed i"
unfolding division_of_def by fastforce
-subsection \<open>General bisection principle for intervals; might be useful elsewhere.\<close>
+subsection \<open>General bisection principle for intervals; might be useful elsewhere\<close>
lemma interval_bisection_step:
fixes type :: "'a::euclidean_space"
@@ -2185,7 +2185,7 @@
qed
-subsection \<open>Cousin's lemma.\<close>
+subsection \<open>Cousin's lemma\<close>
lemma fine_division_exists:
fixes a b :: "'a::euclidean_space"
@@ -2231,7 +2231,7 @@
obtains p where "p tagged_division_of {a .. b}" "g fine p"
by (metis assms box_real(2) fine_division_exists)
-subsection \<open>A technical lemma about "refinement" of division.\<close>
+subsection \<open>A technical lemma about "refinement" of division\<close>
lemma tagged_division_finer:
fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Apr 09 16:20:23 2018 +0200
@@ -4,7 +4,7 @@
Author: Brian Huffman, Portland State University
*)
-section \<open>Elementary topology in Euclidean space.\<close>
+section \<open>Elementary topology in Euclidean space\<close>
theory Topology_Euclidean_Space
imports
@@ -1873,7 +1873,7 @@
by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
qed
-subsection \<open>Intervals in general, including infinite and mixtures of open and closed.\<close>
+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)"
@@ -5653,7 +5653,7 @@
shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
using assms continuous_on_closed by blast
-subsection%unimportant \<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%unimportant \<open>Topological properties of linear functions.\<close>
+subsection%unimportant \<open>Topological properties of linear functions\<close>
lemma linear_lim_0:
assumes "bounded_linear f"