BanachSpace concept

A Banach space is a VectorSpace. A VectorSpace becomes a Banach space if it is equipped with a norm, denoted by ||x||.

In addition to those defined by VectorSpace:

real_type: the result of the norm function

`X`	A type that is a model of BanachSpace
`v`	Object of type `X`

In addition to those defined by VectorSpace:

Name	Expression	Type requirements	Return type
Norm	`v.norm()`		`real_type`

Name	Expression	Precondition	Semantics	Postcondition
Norm	`v.norm()`			`v.norm() ≥ 0`