| 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 3999), but
this is not required. For example, F = { ⟨
2 , 6 ⟩, ⟨
3 , 9 ⟩ } -> ( F ‘ 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.) |
