| Description: Define the range of a
class. For example,
𝐹 =
{⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9} (ex-rn 30802).
Contrast with domain (defined in df-dm 5670). For alternate definitions,
see dfrn2 5877, dfrn3 5878, and dfrn4 6200. The notation "ran " is used
by Enderton. The range of a function is often also called "the
image of
the function" (see definition in [Lang] p. ix), which can be justified
by imadmrn 6071. Not to be confused with
"codomain" (see df-f 6540), which
may be a superset/superclass of the range (see frn 6713).
(Contributed by
NM, 1-Aug-1994.) |
