Metamath Proof Explorer


Syntax definition crli

Description: Extend class notation with real convergence relation for limits.

Ref Expression
Assertion crli class