Definition talk:Image (Relation Theory)/Mapping/Element

is the image of an element an element or a set (singleton)?

I think there is an inconsistency in

$\Img s = \map f s = \bigcup \set {\ldots}$

• $\map f s$ should be an element the codomain of $f$, but
• $\bigcup \set {\ldots}$ is a set of such elements.

Although, it's specified under that the value is unique and well-defined, the definition isn't coherent in respect to the typing.

Is the part '$= \bigcup \set {\ldots}$' really needed / adding some valuable info here? Austrodata (talk) 17:50, 20 February 2025 (UTC)

You could well have a point.

The $\bigcup$ came in here:

https://proofwiki.org/w/index.php?title=Definition%3AImage_%28Relation_Theory%29%2FMapping%2FElement&type=revision&diff=102395&oldid=96634

Not sure why. We have cause to mistrust the exposition generated from the Takeuti and Zaring work.

This may add some context as to why it was originally defined as a set in the first place:

Definition:Image (Relation Theory)/Relation/Element

I'll give it some thought in due course, but in the meantime leave it open to others to weigh in. --prime mover (talk) 20:12, 20 February 2025 (UTC)

I see. Thanks for the investigation.

This must be definition 6.11 to 6.14, p26-27, 2nd ed. of Takeuti and Zaring.

As far as I can understand they are consistent about this but only define $A'b$ as a set, noting that it is a singleton (but this book is very hard to read for me, partly because it contains a lot of unusual notation).

That said, I've done a quick check among the books I've at hand and I only found one which explicitly define the concept of 'the image of an element under a function': Goldrei, Classic Set Theory for Guided Independent Study, 1996. The other ones don't bother with this and only define the image of a subset. Austrodata (talk) 21:40, 20 February 2025 (UTC)

I wonder whether to shrug it aside with an "also defined as" page which defines it as an element rather than as a set, and casually dismiss it by saying something like "$\mathsf{Pr} \infty \mathsf{fWiki}$ may use either convention, and which one is clear from its context" or something, noting that by definition of a function, the image is a singleton, as you allude to above.

Alternatively we define it as an element, but then define the singleton image as the image set.

But it would be a shame to lose the compatibility of the definition of the image of an element under a function with that under a relation. --prime mover (talk) 22:37, 20 February 2025 (UTC)