Meaning of "JFM"

[Alexander van der Vekens]

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.

[Glauco]

Using Gemini and some luck, could it be Journal Of Formalized Mathematics ?

[Mario Carneiro]

Yes, these are references to the Mizar Mathematical Library, as published in the Journal of Formalized Mathematics.

On Sat, Mar 30, 2024 at 4:58 PM Glauco <glaform...@gmail.com> wrote:

Using Gemini and some luck, could it be Journal Of Formalized Mathematics ?

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/72adc053-0dee-4621-b669-72b5bc0536dbn%40googlegroups.com.