src/HOL/Analysis/Linear_Algebra.thy
changeset 69600 86e8e7347ac0
parent 69597 ff784d5a5bfb
child 69619 3f7d8e05e0f2
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sat Jan 05 20:12:02 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun Jan 06 12:32:01 2019 +0100
     1.3 @@ -183,7 +183,9 @@
     1.4  
     1.5  subsection \<open>Bilinear functions\<close>
     1.6  
     1.7 -definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
     1.8 +definition%important
     1.9 +bilinear :: "('a::real_vector \<Rightarrow> 'b::real_vector \<Rightarrow> 'c::real_vector) \<Rightarrow> bool" where
    1.10 +"bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
    1.11  
    1.12  lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
    1.13    by (simp add: bilinear_def linear_iff)
    1.14 @@ -239,7 +241,8 @@
    1.15  
    1.16  subsection \<open>Adjoints\<close>
    1.17  
    1.18 -definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
    1.19 +definition%important adjoint :: "(('a::real_inner) \<Rightarrow> ('b::real_inner)) \<Rightarrow> 'b \<Rightarrow> 'a" where
    1.20 +"adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
    1.21  
    1.22  lemma adjoint_unique:
    1.23    assumes "\<forall>x y. inner (f x) y = inner x (g y)"