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