Syntax Definition ccv 4981

Description: Extend class notation with the covers relation on a Hilbert lattice.

Assertion

Ref	Expression
ccv	class ⋖

See definition df-cv 5712 for more information.

metamath.org