Metamath Proof Explorer


Syntax definition clsxlim

Description: Extend class notation with convergence relation for limits in the extended real numbers.

Ref Expression
Assertion clsxlim class ~~>*