Characterization theorems (~ is*)

[Benoit]

Many theorems in set.mm are characterizations of elements of a defined class.  For instance: ~isgrp , ~ istopg .  More precisely, if we have a definition

df-xxx $a |- Class = { x | Phi } $.

Then there is typically in set.mm a theorem isxxx.  If Phi(A) does not imply that A is a set, then there are two possible forms:

isxxx1 $p |- ( A e. Class <-> ( A e. _V /\ Phi(A) ) )

isxxx2 $p |- ( A e. V -> ( A e. Class <-> Phi(A) ) )

It is easy to go back and forth (using biadan2 and baib).

Is there a preferred form ?  Is it ok to have both in set.mm ?  It seems to me that isxxx1 is closer to a real characterization (while isxxx2 is a characterization among sets), but after a quick look, it seems that isxxx2 is often (majoritarily?) used in set.mm, for instance by looking at the number of usages of elab2g versus elab4g.

Benoît

[Scott Fenton]

I've generally gone with el* in my mathbox (see, eg., elno). I've seen is* around, but I feel el* has better compatibility with el*ab*.

--
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/f8248f4c-ea12-4b44-b6e7-dee1e5db3feen%40googlegroups.com.

[Alexander van der Vekens]

(This topic was discussed in the comments for Github PR #2344: https://github.com/metamath/set.mm/pull/2344)

I'am also often uncertain which of these variants to use. ~isxxx1 is more powerful because it is a biconditional, but  ~isxxx2 is easier to use/understand. Maybe we can agree on a fixed order if both variants are available. I would prefer to have ~isxxx1 first, followed by ~isxxx2 which is proven by using ~isxxx1 and ~biadan2 . The first theorem (~isxxx1 ) should be named isxxxb ("b" for "biconditional" - see conventions for Suffixes"), the second theorem (~isxxx2) should be named isxxx. The comment of  ~isxxx1 (resp.  ~isxxxb) shoud be in the form "The predicate "is a ...". ", and the comment of  ~isxxx2 (resp.  ~isxxx) "The predicate "is a ..." for a set.".

I would prefer the prefix "is" over "el", because it is more general. For example ~iswlk has the form " .. -> ( F ( Walks ` G ) P <-> ..", which does not contain an ` e. ` ("is element of"). But I don't want to hide that you can write this theorem in the form " .. -> ( <. F ,  P >. e. ( Walks ` G ) <-> .." ...

[Benoit]

I agree, except maybe for the suffix "b", which should not be automatic as soon as a statement is a biconditional.  A characterization is by definition a biconditional.  If there is only one form of isxxx in set.mm, then use that default label, and if both forms are in set.mm, then maybe use "isxxx" and "isxxxs" (for "isxxx for sets") ?