Database
BASIC ALGEBRAIC STRUCTURES
Generalized pre-Hilbert and Hilbert spaces
Orthocomplements and closed subspaces
cthl
Next ⟩
df-ocv
Metamath Proof Explorer
Ascii
Structured
Syntax definition
cthl
Description:
Extend class notation with the Hilbert lattice.
Ref
Expression
Assertion
cthl
class
toHL