Class

Class function

A class function1 is a generalization of a set function, such that the domain may be any Class #m/def/set Exactly how this is treated depends on the axiomatic set theory employed, but generally one takes a Relation class with the restriction that each element in the domain is related to exactly one element in the codomain. Thus in NBG

𝔉𝔫𝔠⁡(𝐹)⟺ℜ𝔢𝔩⁡(𝐹)∧(∀𝑥)(∀𝑦)[(𝑥,𝑦)∈𝐹∧(𝑥,𝑧)∈𝐹⟹𝑦=𝑧]

while in ZF we may treat the notion indirectly by a predicative formula 𝜑(𝑥,𝑦) such that

(∀𝑥)(∀𝑦)[𝜑(𝑥,𝑦)∧𝜑(𝑥,𝑧)⟹𝑦=𝑧]

#state/tidy | #lang/en | #SemBr

Footnotes

  1. Not to be confused with a group class function, which is often referred to by the same name. ↩