Definition 1.4.4.  Let S, T be sets, ≺ be a relation from S to T. We define:
≺ is a mapping  :⇔  ∀ s ∈ S : ∃! t ∈ T : s ≺ t
Remarks.

In this library, "mapping" and "function" are not synonymous but interchangeable, via a definition that transforms a mapping to a function (see $../Functions/"mapping as function"). The difference is not fundamental but a matter of convenience.

References.