Metamath Proof Explorer


Syntax definition chlim

Description: Direct limit structure.

Ref Expression
Assertion chlim class HomLim