src/HOL/Library/Inner_Product.thy
changeset 31414 8514775606e0
parent 31289 847f00f435d4
child 31417 c12b25b7f015
equal deleted inserted replaced
31413:729d90a531e4 31414:8514775606e0
     8 imports Complex_Main FrechetDeriv
     8 imports Complex_Main FrechetDeriv
     9 begin
     9 begin
    10 
    10 
    11 subsection {* Real inner product spaces *}
    11 subsection {* Real inner product spaces *}
    12 
    12 
    13 class real_inner = real_vector + sgn_div_norm + dist_norm +
    13 class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
    14   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    14   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    15   assumes inner_commute: "inner x y = inner y x"
    15   assumes inner_commute: "inner x y = inner y x"
    16   and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
    16   and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
    17   and inner_scaleR_left: "inner (scaleR r x) y = r * (inner x y)"
    17   and inner_scaleR_left: "inner (scaleR r x) y = r * (inner x y)"
    18   and inner_ge_zero [simp]: "0 \<le> inner x x"
    18   and inner_ge_zero [simp]: "0 \<le> inner x x"