| Description: Define the value of a
function, (𝐹‘𝐴), also known as function
application. For example, ( I ‘∅) =
∅. Typically,
function 𝐹 is defined using maps-to notation
(see df-mpt 4096), but
this is not required. For example,
𝐹 =
{⟨2, 6⟩, ⟨3, 9⟩} → (𝐹‘3) = 9. We will later
define two-argument functions using ordered pairs as
(𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩). This particular definition
is
quite convenient: it can be applied to any class and evaluates to the
empty set when it is not meaningful. The left apostrophe notation
originated with Peano and was adopted in Definition *30.01 of
[WhiteheadRussell] p. 235,
Definition 10.11 of [Quine] p. 68, and
Definition 6.11 of [TakeutiZaring]
p. 26. It means the same thing as
the more familiar 𝐹(𝐴) notation for a function's value at
𝐴,
i.e., "𝐹 of 𝐴," but without
context-dependent notational
ambiguity. (Contributed by NM, 1-Aug-1994.) Revised to use ℩.
(Revised by Scott Fenton, 6-Oct-2017.) |
