Library Coqtail.Topology.Inner_product

Require Import Vectors.
Require Import Reals.

Section Euclidean_Space.
  Variable (V:Type) (vO:V).
  Variable vadd : V→V→V.
  Variable smul : R→V→V.
  Variable v : vector_space R (1%R) Rplus Rmult V vO vadd smul.
  Variable inner : V→V→R.

  Record eucledian_space : Type := {
    euclidean_conjugate_symmetry : ∀ x y, inner x y = inner y x;
    euclidean_left_linearity_mult : ∀ a x y, inner (smul a x) y = Rmult a (inner x y);
    euclidean_left_linearity_plus : ∀ x y z, inner (vadd x y) z = inner (vadd x z) (vadd y z);
    euclidean_positiveness : ∀ x, (inner x x ≥ 0)%R;
    euclidean_definiteness : ∀ x, inner x x = 0%R → x = vO
  }.
End Euclidean_Space.