Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Hilbert lattices
chlt
Next ⟩
df-hlat
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
chlt
Description:
Extend class notation with Hilbert lattices.
Ref
Expression
Assertion
chlt
class
HL