tuned
authornipkow
Mon Sep 03 22:38:23 2018 +0200 (8 months ago)
changeset 689014824cc40f42e
parent 68900 1145b25c53de
child 68902 8414bbd7bb46
tuned
src/HOL/Analysis/Linear_Algebra.thy
     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"