Metamath Proof Explorer


Syntax definition clan

Description: Class function defining the (local) left Kan extension.

Ref Expression
Assertion clan
class Lan