Content deleted Content added
Joel Brennan (talk | contribs) m →Size of sets: added wikilinks |
→Functions: Fixed typo in the range of a relation |
||
Line 93:
Outside of formal set theory, we usually specify a function in terms of its ___domain and codomain, as in the phrase "Let <math>f: A \to B</math> be a function". The ___domain of a function is just its ___domain as a relation, but we have not yet defined the codomain of a function. To do this we introduce the terminology that a function is '''from <math>A</math> to <math>B</math>''' if its ___domain equals <math>A</math> and its range ''is contained in'' <math>B</math>. In this way, every function is a function from its ___domain to its range, and a function <math>f</math> from <math>A</math> to <math>B</math> is also a function from <math>A</math> to <math>C</math> for any set <math>C</math> containing <math>B</math>.
Indeed, no matter which set we consider to be the codomain of a function, the function does not change as a set since by definition it is just a set of ordered pairs. That is, a function does not determine its codomain by our definition. If one finds this unappealing then one can instead define a function as the ordered pair <math>(f, B)</math>, where <math>f</math> is a functional relation and <math>B</math> is its codomain, but we do not take this approach in this article (more elegantly, if one first defines ordered triples - for example as <math>(x, y, z) = (x, (y, z))</math>- then one could define a function as the ordered triple <math>(f, A, B)</math> so as to also include the ___domain). Note that the same issue exists for relations: outside of formal set theory we usually say "Let <math>R \subseteq A \times B</math> be a binary relation", but formally <math>R</math> is a set of ordered pairs such that <math>\text{dom}\,R \subseteq A</math> and <math>\text{ran}\,R \subseteq
In NFU, <math>x</math> has the same type as <math>F\!\left(x\right)</math>, and <math>F</math> is three types higher than <math>F\!\left(x\right)</math> (one type higher, if a type-level ordered pair is used). To solve this problem, one could define <math>F\left[A\right]</math> as <math>\left\{y : \exists x\,\left(x \in A \wedge y = F\!\left(x\right)\right)\right\}</math> for any set <math>A</math>, but this is more conveniently written as <math>\left\{F\!\left(x\right) : x \in A\right\}</math>. Then, if <math>A</math> is a set and <math>F</math> is any functional relation, the [[Axiom of replacement|Axiom of Replacement]] assures that <math>F\left[A\right]</math> is a set in [[ZFC]]. In NFU, <math>F\left[A\right]</math> and <math>A</math> now have the same type, and <math>F</math> is two types higher than <math>F\left[A\right]</math> (the same type, if a type-level ordered pair is used).
| |||