Database
BASIC ALGEBRAIC STRUCTURES
Generalized pre-Hilbert and Hilbert spaces
Orthogonal projection and orthonormal bases
cobs
Next ⟩
df-pj
Metamath Proof Explorer
Unicode
Structured
Syntax definition
cobs
Description:
Extend class notation with the set of orthonormal bases.
Ref
Expression
Assertion
cobs
class OBasis