Metamath Proof Explorer


Syntax definition cflim

Description: Extend class notation with a function returning the limit of a filter.

Ref Expression
Assertion cflim
class fLim