Revision as of 20:09, 25 October 2019 edit Joel Brennan (talk \| contribs) Extended confirmed users 3,724 edits →Functions: explained more clearly that a function does not determine its codomain ← Previous edit		Revision as of 20:10, 25 October 2019 edit undo Joel Brennan (talk \| contribs) Extended confirmed users 3,724 edits →Related definitions: has been moved into the 'functions' section Next edit →
Line 66: The '''[[relation composition\|relative product]]''' <math>R\|S</math> of <math>R</math> and <math>S</math> is the relation <math>\left\{\left(x, z\right) : \exists y\,\left(xRy \wedge ySz\right)\right\}</math>. In ZFC, one proves that these notions all generate or apply to sets via the ZFC axioms of ''Union'', ''Separation'', and ''[[Axiom of power set\|Power set]]''. In NFU, it is easy to check that these definitions give rise to stratified formulas. Notice that with our formal definition of a binary relation, the range and codomain of a relation are not distinguished. This could be done by representing a relation <math>R</math> with codomain <math>B</math> as <math>\left(R, B\right)</math>, but our development will not require this.

Implementation of mathematics in set theory: Difference between revisions