Database
BASIC ALGEBRAIC STRUCTURES
Generalized pre-Hilbert and Hilbert spaces
Orthogonal projection and orthonormal bases
cpj
Next ⟩
chil
Metamath Proof Explorer
Ascii
Structured
Syntax definition
cpj
Description:
Extend class notation with orthogonal projection function.
Ref
Expression
Assertion
cpj
class
proj