Line 2,560: |
Line 2,560: |
| Thus, we arrive by way of this winding stair at the very special stamps of 2-adic relations ''P'' ⊆ ''X'' × ''Y'' that are "total prefunctions" at ''X'' (or ''Y''), "total and tubular" at ''X'' (or ''Y''), or "1-regular" at ''X'' (or ''Y''), more often celebrated as "functions" at ''X'' (or ''Y''). | | Thus, we arrive by way of this winding stair at the very special stamps of 2-adic relations ''P'' ⊆ ''X'' × ''Y'' that are "total prefunctions" at ''X'' (or ''Y''), "total and tubular" at ''X'' (or ''Y''), or "1-regular" at ''X'' (or ''Y''), more often celebrated as "functions" at ''X'' (or ''Y''). |
| | | |
− | <pre> | + | <blockquote> |
− | | If P is a pre-function P : X ~> Y that happens to be total at X, then P
| + | <p>If ''P'' is a pre-function ''P'' : ''X'' ~> ''Y'' that happens to be total at ''X'', then ''P'' is known as a "function" from ''X'' to ''Y'', typically indicated as ''P'' : ''X'' → ''Y''.</p> |
− | | is known as a "function" from X to Y, typically indicated as P : X -> Y.
| + | |
− | |
| + | <p>To say that a relation ''P'' ⊆ ''X'' × ''Y'' is totally tubular at ''X'' is to say that it is 1-regular at ''X''. Thus, we may formalize the following definitions:</p> |
− | | To say that a relation P c X x Y is totally tubular at X is to say that
| + | |
− | | it is 1-regular at X. Thus, we may formalize the following definitions:
| + | :{| cellpadding="4" |
− | | | + | | ''P'' is a "function" ''p'' : ''X'' → ''Y'' |
− | | P is a "function" p : X -> Y iff P is 1-regular at X. | + | | iff |
− | | | + | | ''P'' is 1-regular at ''X''. |
− | | P is a "function" p : X <- Y iff P is 1-regular at Y. | + | |- |
| + | | ''P'' is a "function" ''p'' : ''X'' ← ''Y'' |
| + | | iff |
| + | | ''P'' is 1-regular at ''Y''. |
| + | |} |
| + | </blockquote> |
| | | |
− | For example, let X = Y = {0, ..., 9} and let F c X x Y be | + | For example, let ''X'' = ''Y'' = {0, …, 9} and let ''F'' ⊆ ''X'' × ''Y'' be the 2-adic relation that is depicted in the bigraph below: |
− | the 2-adic relation that is depicted in the bigraph below: | |
| | | |
| + | <pre> |
| 0 1 2 3 4 5 6 7 8 9 | | 0 1 2 3 4 5 6 7 8 9 |
| o o o o o o o o o o X | | o o o o o o o o o o X |
Line 2,581: |
Line 2,586: |
| o o o o o o o o o o Y | | o o o o o o o o o o Y |
| 0 1 2 3 4 5 6 7 8 9 | | 0 1 2 3 4 5 6 7 8 9 |
| + | </pre> |
| | | |
− | We observe that F is a function at Y, | + | We observe that ''F'' is a function at ''Y'', and we record this fact in either of the manners ''F'' : ''X'' ← ''Y'' or ''F'' : ''Y'' → ''X''. |
− | and we record this fact in either of | |
− | the manners F : X <- Y or F : Y -> X. | |
− | </pre>
| |
| | | |
| ===Commentary Note 11.10=== | | ===Commentary Note 11.10=== |