| Description: Extend the definition of
a class to include the value of a function.
Read: "the value of 𝐹 at 𝐴 " or "𝐹 of
𝐴". In a
previous version, the symbol " ' " was used. However, since the
similarity with the symbol ‘ used for the
current definition of a
function's value (see df-fv 6569), which, by the way, was intended to
visualize that in many cases ‘ and " '
" are exchangeable, makes
reading the theorems, especially those which use both definitions as
dfafv2 47144, very difficult, 3 apostrophes ''' are used now so that it's
easier to distinguish from df-fv 6569 and df-ima 5698. And not three backticks
( three times ‘) since that would be
annoying to escape in a
comment. (See remark of Norman Megill and Gerard Lang at
https://groups.google.com/g/metamath/c/cteNUppB6A4 5698). |
