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 25698
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.
Assertion
Ref Expression
copfn  class  opfn

See definition df-opfn 25699 for more information.

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