src/HOL/Analysis/Linear_Algebra.thy
 changeset 68901 4824cc40f42e parent 68607 67bb59e49834 child 69510 0f31dd2e540d
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Mon Sep 03 20:46:09 2018 +0200
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Sep 03 22:38:23 2018 +0200
1.3 @@ -31,7 +31,7 @@
1.4    using finite finite_image_set by blast
1.5
1.6
1.7 -subsection%unimportant \<open>More interesting properties of the norm.\<close>
1.8 +subsection%unimportant \<open>More interesting properties of the norm\<close>
1.9
1.10  notation inner (infix "\<bullet>" 70)
1.11
1.12 @@ -131,7 +131,7 @@
1.13  qed simp
1.14
1.15
1.16 -subsection \<open>Orthogonality.\<close>
1.17 +subsection \<open>Orthogonality\<close>
1.18
1.19  definition%important (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
1.20
1.21 @@ -200,7 +200,7 @@
1.22  qed
1.23
1.24
1.25 -subsection \<open>Bilinear functions.\<close>
1.26 +subsection \<open>Bilinear functions\<close>
1.27
1.28  definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
1.29
1.30 @@ -256,7 +256,7 @@
1.31  qed
1.32
1.33
1.34 -subsection \<open>Adjoints.\<close>
1.35 +subsection \<open>Adjoints\<close>
1.36
1.37  definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
1.38
1.39 @@ -658,7 +658,7 @@
1.40    by (metis linear_imp_has_derivative differentiable_def)
1.41
1.42
1.43 -subsection%unimportant \<open>We continue.\<close>
1.44 +subsection%unimportant \<open>We continue\<close>
1.45
1.46  lemma independent_bound:
1.47    fixes S :: "'a::euclidean_space set"
```