Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  copfn Unicode version

Syntax Definition copfn 25595
Description: Extend class notation with an operator that derives an operation on functions from an operation on the elements of the common range of those functions.
Ref Expression
copfn  class  opfn

See definition df-opfn 25596 for more information.

Colors of variables: wff set class
  Copyright terms: Public domain W3C validator