Metamath Proof Explorer


Syntax definition ctrl

Description: Extend class notation with set of all traces of lattice translations.

Ref Expression
Assertion ctrl class trL