Description: Define the value of a
function, (𝐹‘A), also known as function
application. For example, ( I ‘∅) =
∅. Typically,
function 𝐹 is defined using maps-to notation
(see df-mpt 3811), 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
(A𝐹B) =
(𝐹‘⟨A, B⟩). 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 𝐹(A) notation for a function's value at A,
i.e. "𝐹 of A," but without context-dependent
notational
ambiguity. (Contributed by NM, 1-Aug-1994.) Revised to use ℩.
(Revised by Scott Fenton, 6-Oct-2017.) |