Metamath Proof Explorer


Syntax definition cmri

Description: mrInd is a class function which takes a Moore system to its set of independent sets.

Ref Expression
Assertion cmri class mrInd