This is an inofficial mirror of
http://metamath.tirix.org
for personal testing of a visualizer extension only.
Database
BASIC ALGEBRAIC STRUCTURES
Generalized pre-Hilbert and Hilbert spaces
Orthocomplements and closed subspaces
cthl
Next ⟩
df-ocv
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cthl
Description:
Extend class notation with the Hilbert lattice.
Ref
Expression
Assertion
cthl
class
toHL