Does anybody know what the abbreviation "JFM" means? It appears several
times in set.mm, for example:
$( The Cartesian product of two elements of a transitive Tarski class is an
element of the class. JFM CLASSES2 th. 67 (partly). (Contributed by
FL,
15-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.) $)
tskxp $p |- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ B e. T ) -> ( A X. B
) e. T ) $=
or
$( Function returning the epimorphisms of the category ` c ` . JFM
CAT_1
def. 11. (Contributed by FL, 8-Aug-2008.) (Revised by Mario
Carneiro,
2-Jan-2017.) $)
df-epi $a |- Epi = ( c e. Cat |-> tpos ( Mono ` ( oppCat ` c ) ) ) $.
Furthermore, there is a link to ~
http://www.mizar.org/JFM/Axiomatics/tarski.html , but this link is broken.
But http://mizar.org/JFM/ exists and is titled "Journal of Formalized
Mathematics" (I think this is the meaning of "JFM").
If I am right, the broken link should be fixed, and the other references
should be explained (at least at the first occurence of JFM CLASSES1, JFM
CLASSES2, and JFM CAT_1) or should be replaced by other references into the
literature.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/3df85c4a-c8e0-456a-b07c-fcb293338305n%40googlegroups.com.
