pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` A ) ) ErALTV A ) Partition-Equivalence Theorem with general ` R `

[Mázsa Péter]

Dear Community,


First of all, let me express my deep sadness at the death of Norman.
The community explained the significance of his legacy already: all I
can do is add my own personal perspective. Without the - both machine
and human readable - system of Metamath, which gives constant
feedback, and accumulates knowledge, I would never have been able to
think systematically and coherently about mathematics. He helped me,
along with many other great people from the fantastic community he
founded and carefully raised, to continue my first precarious steps in
set theory.
His idea and his efforts survive him.
Thank you Norman.

_
My purpose in set theory was to reveal the Partition-Equivalence
Theorem with general ` R `. My results are attached as a Mathbox.
Proofs and markup are verified, but I need some theorems of Thierry
Arnoux, Scott Fenton, Frédéric Liné, Rodolfo Medina and Richard
Penner, and my latexdefs, htmldefs and althtmldefs, in the main part
of set.mm. Some theorems are slight modifications of theorems of Mario
Carneiro, Rodolfo Medina and Norman Megill.

Since the attached Mathbox is quite long (600+ necessary and
sufficient definitions and theorems incl. versions), I‘ll now give you
a summary. I’d like to discuss my results here on the email-list.

I had to redefine some basic concepts (e.g. reflexivity, symmetry,
transitivity, equivalence relation and equivalence relation with
domain part, function, disjointness and partition), and suggest a new
one (converse reflexivity), in order to reach the
Partition-Equivalence Theorem.
This motivation is very important here: I’m aware of the discussion
https://github.com/metamath/set.mm/pull/1286 with the participation of
Thierry Arnoux, Benoit Jubin, Normann Megill and David A. Wheeler, and
if you find better definitions for reflexivity etc. than me, I do not
oppose them from the outset. However it would be great if
1. At least reflexivity, symmetry and transitivity had coherent
definitions (compare ~ df-refs and ~ df-syms below, as opposed to ~
issref with ` A ` vs. ~ cnvsym without ` A ` in set.mm),
2. Based on the 2. requirement of the Guidelines at
http://us.metamath.org/mpeuni/mathbox.html all concepts were defined
primarily as 0-ary class constants (like ~ df-refrels ),
3. Moreover, all class constants had a corresponding predicate for
proper classes (like ~ df-refrel for _I in ~ refrelid $p |- RefRel _I
) so that e.g. in case of reflexive relations, the element of the
class of all reflexive relations ( ~ elrefrels2 ) and the reflexive
relation predicate ( ~ df-refrel ) were the same when ` R ` is a set:
~ elrefrelsrel $p |- ( R e. V -> ( R e. RefRels <-> RefRel R ) ) ,
4. You proved that they reproduce at least ~ mpet $p |- ( MembPart A
<-> MembEr A ) , ~ pet and ~ pets , or their (possible future)
generalization, ` gpet ` , see below.

After the (new, suggested) definitions you’ll find the (old)
definitions which are presently in set.mm or in a Mathbox (
https://github.com/metamath/set.mm/blob/develop/set.mm ).

_
Classes of all reflexive, converse reflexive, symmetric, transitive
sets (new, suggested definitions, used only once in ~ df-refrels , ~
df-cnvrefrels , ~ df-symrels and ~ df-trrels below):
df-refs $a |- Refs = { x | ( _I i^i ( dom x X. ran x ) ) _S ( x i^i (
dom x X. ran x ) ) }
df-cnvrefs $a |- CnvRefs = { x | ( _I i^i ( dom x X. ran x ) ) `' _S (
x i^i ( dom x X. ran x ) ) } (new concept, we need it below at
functions and disjoints)
df-syms $a |- Syms = { x | `' ( x i^i ( dom x X. ran x ) ) _S ( x i^i
( dom x X. ran x ) ) }
df-trs $a |- Trs = { x | ( ( x i^i ( dom x X. ran x ) ) o. ( x i^i (
dom x X. ran x ) ) ) _S ( x i^i ( dom x X. ran x ) ) }
where ` _S ` is the subsets class, or the class of the subset
relations (new, suggested definition):
df-ssr $a |- _S = { <. x , y >. | x C_ y } , or ` df-ss `, since the
present ~ df-ss definition of the subclass relation ` A C_ B ` should
be relabeled as ` df-sc `.
Scott Fenton's subset class ~ df-sset and ` _S ` are the same
ssreqsset $p |- _S = SSet ,
however, the notation ` _S ` and the construction of ~ df-ssr reveals
its similarity to these old definitions in set.mm:
df-id $a |- _I = { <. x , y >. | x = y } and
df-eprel $a |- _E = { <. x , y >. | x e. y } .

Classes of all reflexive, etc. relations (new, suggested):
df-refrels $a |- RefRels = ( Refs i^i Rels )
df-cnvrefrels $a |- CnvRefRels = ( CnvRefs i^i Rels )
df-symrels $a |- SymRels = ( Syms i^i Rels )
df-trrels $a |- TrRels = ( Trs i^i Rels )
where the relations class (new, suggested) is
df-rels $a |- Rels = ~P ( _V X. _V ) .

In predicate form the above definitions give:
dfrefrel2 $p |- ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )
! dfrefrel3 $p |- ( RefRel R <-> ( A. x e. dom R A. y e. ran R ( x = y
-> x R y ) /\ Rel R ) )
dfcnvrefrel2 $p |- ( CnvRefRel R <-> ( R C_ ( _I i^i ( dom R X. ran R
) ) /\ Rel R ) )
dfcnvrefrel3 $p |- ( CnvRefRel R <-> ( A. x e. dom R A. y e. ran R ( x
R y -> x = y ) /\ Rel R ) )
dfsymrel2 $p |- ( SymRel R <-> ( `' R C_ R /\ Rel R ) )
dfsymrel3 $p |- ( SymRel R <-> ( A. x A. y ( x R y -> y R x ) /\ Rel R ) )
dftrrel2 $p |- ( TrRel R <-> ( ( R o. R ) C_ R /\ Rel R ) )
dftrrel3 $p |- ( TrRel R <-> ( A. x A. y A. z ( ( x R y /\ y R z ) ->
x R z ) /\ Rel R ) )
Note that while ` Rel R ` cancels restriction of ` R ` , it keeps
restriction of ` _I ` : this is why the very similar definitions ~
df-refs , ~ df-syms and ~ df-trs diverge when we switch from (general)
sets to relations in ~ dfrefrel* , ~ dfsymrel* and ~ dftrrel* .

Reflexivity and symmetry reproduce ` x R x ` for the reflexivity part,
but only together:
refsymrel2 $p |- ( ( RefRel R /\ SymRel R ) <-> ( ( ( _I |` dom R ) C_
R /\ `' R C_ R ) /\ Rel R ) )
! refsymrel3 $p |- ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R x
R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )
Reflexivity and symmetry are often bound together in equivalence
relation. Reflexivity may be perceived primarily as a necessary part
of equivalence. This seems to be the main reason why we thought so far
that reflexivity on its own should be defined like the reflexivity
part of ~ dfeqvrel3 below, i.e., by using the apparently self-evident
` x R x ` form.
Another possible reason is that we are inclined to constrain ourselves
to convenient special cases where the two forms are equivalent, e.g.
the one with square Cartesian product:
idinxpssinxp3 $p |- ( ( _I i^i ( A X. A ) ) C_ ( R i^i ( A X. A ) )
<-> ( _I |` A ) C_ R ) and
idinxpssinxp4 $p |- ( A. x e. A A. y e. A ( x = y -> x R y ) <-> A. x
e. A x R x ) .

Old reflexivity versions in set.mm or in a Mathbox now, with ` x R x `:
df-reflexive $a |- ( R Reflexive A <-> ( R C_ ( A X. A ) /\ A. x e. A x R x ) )
issref $p |- ( ( _I |` A ) C_ R <-> A. x e. A x R x )

Equivalence relations (new, suggested for set.mm, but other math
sources seem to define it in a way which is similar to this one):
df-eqvrels $a |- EqvRels = ( ( RefRels i^i SymRels ) i^i TrRels )
which gives
dfeqvrel2 $p |- ( EqvRel R <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R
/\ ( R o. R ) C_ R ) /\ Rel R ) )
dfeqvrel3 $p |- ( EqvRel R <-> ( ( A. x e. dom R x R x /\ A. x A. y (
x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
/\ Rel R ) )
There is no comparable definition of equivalence relation now in set.mm.

Equivalence relations with domain part (new, suggested):
df-ers $a |- Ers = ( DomainQss |` EqvRels )
where df-dmqss $a |- DomainQss = { <. x , y >. | ( dom x /. x ) = y }
which gives
dferALTV2 $p |- ( R ErALTV A <-> ( EqvRel R /\ ( dom R /. R ) = A ) )
This definition implies that the natural domain of equivalence relations
is not ` R Domain A ` (i.e. ` dom R = A ` cf. ~ brdomaing ), like in
the present ~ df-er in set.mm,
but ` R DomainQss A ` (i.e. ` ( dom R /. R ) = A ` , cf. ~ brdmqss ),
"domain quotients".
The main reason why I think the new ` R DomainQss A ` to be the
natural domain (and not the old ` R Domain A ` ) is a small set of new
theorems, the Membership Partition-Equivalence Theorems (see mpet*
below) and the Partition-Equivalence Theorems (see pet* below).
Incidentally, with the new definitions above, the old ~ prter3 in set.mm
prter3 $p |- ( ( R Er U. A /\ ( U. A /. R ) = ( A \ { (/) } ) ) -> .~ = R )
simplifies to the new
erALTVimlem $p |- ( R e. V -> ( R ErALTV A -> ~ A = R ) )
where the coelements ` ~ A ` are a special case of cosets ` ,~ R ` :
df-coss $a |- ,~ R = { <. x , y >. | E. u ( u R x /\ u R y ) }
df-coels $a |- ~ A = ,~ ( `' _E |` A )
dfcoels $p |- ~ A = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
While I'm sure we need both equivalence relation ~ df-eqvrels and
equivalence relation on domain quotient ~ df-ers , I'm not sure
whether we need a third equivalence relation concept with the present
` dom R = A ` component as well: this needs further investigation.
Using Occam’s razor I suppose that these two concepts ~ df-eqvrels and
~ df-ers are enough and named the predicate version of the one on
domain quotient as the alternate version ~ df-erALTV of the present ~
df-er (cf. "Alternative (ALTV) versions",
http://us.metamath.org/mpeuni/conventions.html ).

The old definition of equivalence relation (with a domain part) in set.mm
df-er $a |- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
"is not standard" , "somewhat cryptic", has no corresponding costant
0-ary class, does not follow the traditional transparent
reflexive-symmetric-transitive relation way of definition of
equivalence, and fails to deliver the Membership
Partition-Equivalence Theorems and the Partition-Equivalence Theorems.

With the new definitions above comes the
Main Theorem of Equivalences: any equivalence relation implies
equivalent membership as well
mainer $p |- ( R ErALTV A -> MembEr A )
where
df-member $a |- ( MembEr A <-> ~ A ErALTV A )
dfmember3 $p |- ( MembEr A <-> ( EqvRel ~ A /\ ( U. A /. ~ A ) = A ) )

Now we should define functions and disjoints (new, suggested):
df-funss $a |- Funss = { x | ,~ x e. CnvRefRels } , used only once in
df-funsALTV below
df-funsALTV $a |- FunsALTV = ( Funss i^i Rels )
dffunALTV2 $p |- ( FunALTV F <-> ( ,~ F C_ _I /\ Rel F ) )
The new definition of the function predicate ~ df-funALTV (based on a
more general, converse reflexive, relation) and the old definition of
function in set.mm ~ df-fun , are the same:
funALTVfun $p |- ( FunALTV F <-> Fun F )

df-disjss $a |- Disjss = { x | ,~ `' x e. CnvRefRels } , used only
once in df-disjs below
df-disjs $a |- Disjs = ( Disjss i^i Rels )
We need ` Disjs ` and ` Disj R ` for the definition of ` Parts ` and `
R Part A ` for the Partition-Equivalence Theorems: this need for `
Parts ` as disjoint relations on their domain quotients is the reason
why we should define ` Disjs ` instead of simply using converse
functions, cf. ~ pet2 below.
dfdisjALTV2 $p |- ( Disj R <-> ( ,~ `' R C_ _I /\ Rel R ) ) , (read: `
R ` is a disjoint)
dfdisjALTV4 $p |- ( Disj R <-> ( A. x E* u u R x /\ Rel R ) )
dfdisjALTV5 $p |- ( Disj R <-> ( A. u e. dom R A. v e. dom R ( u = v
\/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ Rel R ) )
The old definition of disjointness in set.mm is
df-disj $a |- ( Disj_ x e. A B <-> A. y E* x e. A y e. B )

The disjoint elementhood predicate (read: the elements of ` A ` are
disjoint) is a special case of disjointness (new, suggested):
df-eldisj $a |- ( ElDisj A <-> Disj ( `' _E |` A ) )
dfeldisj5 $p |- ( ElDisj A <-> A. u e. A A. v e. A ( u = v \/ ( u i^i
v ) = (/) ) )
As of now, disjoint elementhood is defined as "partition" in set.mm :
df-prt $a |- ( Prt A <-> A. u e. A A. v e. A ( u = v \/ ( u i^i v ) =
(/) ) ) (cf. the new partition definitions below)
Disjoint elementhood changes
prter1 $p |- ( Prt A -> .~ Er U. A ) of the present set.mm to
mdisjim $p |- ( ElDisj A -> EqvRel ~ A )
and in general form, the
"Divide et Aequivalere" Theorem (new): every disjoint relation
generates equivalent cosets by the relation
disjim $p |- ( Disj R -> EqvRel ,~ R )
Moreover, this changes
prter2 $p |- ( Prt A -> ( U. A /. .~ ) = ( A \ { (/) } ) ) of the
present set.mm to
eldisjn0el $p |- ( ElDisj A -> ( -. (/) e. A <-> ( U. A /. ~ A ) = A ) )
and in general form (new):
disjdmqseq $p |- ( Disj R -> ( ( dom R /. R ) = A <-> ( dom ,~ R /. ,~
R ) = A ) )

Partitions (new, suggested) are disjoints on domain quotients (or:
domain quotients restricted to disjoints):
df-parts $a |- Parts = ( DomainQss |` Disjs ) $.
dfpart2 $p |- ( R Part A <-> ( Disj R /\ ( dom R /. R ) = A ) )
The above definition is a more general meaning of partition than we
accustomed to: the conventional meaning of partition (e.g. partition
` A ` of ` X `, [Halmos] p. 28: "A partition of ` X ` is a disjoint
collection ` A ` of non-empty subsets of ` X ` whose union is ` X ` ",
or Definition 35, [Suppes] p. 83., cf. https://oeis.org/A000110 ) is
what we call here membership partition:
dfmembpart2 $p |- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) , defined as
df-membpart $a |- ( MembPart A <-> ( `' _E |` A ) Part A )

A (somewhat maybe depressing, new) theorem with the membership
partition concept above is the
Theorem of Fences by Equivalences: all kinds of equivalence relations
imaginable (in addition to the membership equivalence relation cf. ~
mpet ) generate partition of the members:
fences $p |- ( R ErALTV A -> MembPart A )

Now we are ready to prove the (new) Membership Partition-Equivalence Theorems:
mpet3 $p |- ( ( ElDisj A /\ -. (/) e. A ) <-> ( EqvRel ~ A /\ ( U. A
/. ~ A ) = A ) )
mpet2 $p |- ( ( `' _E |` A ) Part A <-> ,~ ( `' _E |` A ) ErALTV A )
mpet $p |- ( MembPart A <-> MembEr A )

and the (new) Partition-Equivalence Theorems, with general ` R `:
pet2 $p |- ( ( Disj ( R (x) ( `' _E |` A ) ) /\ ( dom ( R (x) ( `' _E
|` A ) ) /. ( R (x) ( `' _E |` A ) ) ) = A ) <-> ( EqvRel ,~ ( R (x) (
`' _E |` A ) ) /\ ( dom ,~ ( R (x) ( `' _E |` A ) ) /. ,~ ( R (x) ( `'
_E |` A ) ) ) = A ) )
pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |`
A ) ) ErALTV A )
pets $p |- ( ( A e. V /\ R e. W ) ->
( ( R (x) ( `' _E |` A ) ) Parts A <-> ,~ ( R (x) ( `' _E |` A ) ) Ers A ) )
where
br1cosstxpcnvepres $p |- ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) ) ->
( <. B , C >. ,~ ( R (x) ( `' _E |` A ) ) <. D , E >. <->
E. u e. A ( ( C e. u /\ u R B ) /\ ( E e. u /\ u R D ) ) ) )

This small set of theorems is the main result of my investigations in
set theory. ~ pet is not more general than the conventional Membership
Partition-Equivalence Theorem ~ mpet2 (because you cannot set ` R ` in
~ pet in a way that you would get ~ mpet2 ), i.e., this is not the
hypothetical General Partition-Equivalence Theorem ` gpet |- ( R Part
A <-> ,~ R ErALTV A ) `. But ~ pet has a general part that ~ mpet2
lacks: ` R `, which is well enough for my future application of set
theory, for my purpose outside of set theory. Motto: "Le meglio è
l'inimico del bene.":)


Thank you for your attention and consideration:
Peter

[Jim Kingdon]

Hey, thanks for sending those mathbox contributions. I see that you have
been communicating with various people in the past so you are not a
stranger to our community, but in case any of the following helps with
how we generally manage mathboxes, I hope it is helpful.

I don't know how familiar you are with submitting pull requests in
github but just to see how close this submission is to being mergeable
(and in case it helps other people review it), I took what you sent to
the list and put it into github at
https://github.com/metamath/set.mm/pull/2435 . There are a number of
failures there  which I assume do not surprise you (since you talk about
various issues in your email). We've tried to write an intro at
https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing
in case some or all of this git stuff is new to you. If you end up
making your own pull request I can just close this one.

I guess my advice would be to try to get the mathbox in a state where it
can pass the checks and be merged as a mathbox, with relatively few
changes to main at first (even if that means some redundant theorems).
But there might be a bit of a case by case basis for some of these
issues. Hopefully there are some people here who are a bit more up on
these issues than I am because I don't really have a point-by-point
reaction without doing a bunch of research into topics I don't know well.

Glad to hear that metamath has helped you learn set theory. Although I
knew little bits and pieces of set theory (and other topics) before I
got here, contributing to metamath has also been super helpful in terms
of my own understanding, both of topics such as set theory, construction
of real numbers, etc. In particular, my knowledge of constructive
mathematics was quite limited until I started contributing to iset.mm
and I have found that writing theorems there has been quite helpful, but
in aiding my learning directly, and also giving me a push to seek out
sources which I might not otherwise have found.

> df-ssr $a |-_S = { <. x , y >. | x C_ y } , or ` df-ss `, since the

> present ~ df-ss definition of the subclass relation ` A C_ B ` should
> be relabeled as ` df-sc `.
> Scott Fenton's subset class ~ df-sset and ` _S ` are the same
> ssreqsset $p |- _S = SSet ,
> however, the notation ` _S ` and the construction of ~ df-ssr reveals
> its similarity to these old definitions in set.mm:
> df-id $a |- _I = { <. x , y >. | x = y } and
> df-eprel $a |- _E = { <. x , y >. | x e. y } .
>
> Classes of all reflexive, etc. relations (new, suggested):
> df-refrels $a |- RefRels = ( Refs i^i Rels )
> df-cnvrefrels $a |- CnvRefRels = ( CnvRefs i^i Rels )
> df-symrels $a |- SymRels = ( Syms i^i Rels )
> df-trrels $a |- TrRels = ( Trs i^i Rels )
> where the relations class (new, suggested) is
> df-rels $a |- Rels = ~P ( _V X. _V ) .
>
> In predicate form the above definitions give:

> dfrefrel2 $p |- ( RefRel R <-> ( (_I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )

> ! dfrefrel3 $p |- ( RefRel R <-> ( A. x e. dom R A. y e. ran R ( x = y
> -> x R y ) /\ Rel R ) )
> dfcnvrefrel2 $p |- ( CnvRefRel R <-> ( R C_ ( _I i^i ( dom R X. ran R
> ) ) /\ Rel R ) )
> dfcnvrefrel3 $p |- ( CnvRefRel R <-> ( A. x e. dom R A. y e. ran R ( x
> R y -> x = y ) /\ Rel R ) )
> dfsymrel2 $p |- ( SymRel R <-> ( `' R C_ R /\ Rel R ) )
> dfsymrel3 $p |- ( SymRel R <-> ( A. x A. y ( x R y -> y R x ) /\ Rel R ) )
> dftrrel2 $p |- ( TrRel R <-> ( ( R o. R ) C_ R /\ Rel R ) )
> dftrrel3 $p |- ( TrRel R <-> ( A. x A. y A. z ( ( x R y /\ y R z ) ->
> x R z ) /\ Rel R ) )
> Note that while ` Rel R ` cancels restriction of ` R ` , it keeps
> restriction of ` _I ` : this is why the very similar definitions ~
> df-refs , ~ df-syms and ~ df-trs diverge when we switch from (general)
> sets to relations in ~ dfrefrel* , ~ dfsymrel* and ~ dftrrel* .
>
> Reflexivity and symmetry reproduce ` x R x ` for the reflexivity part,
> but only together:

> refsymrel2 $p |- ( ( RefRel R /\ SymRel R ) <-> ( ( (_I |` dom R ) C_

> R /\ `' R C_ R ) /\ Rel R ) )
> ! refsymrel3 $p |- ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R x
> R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )
> Reflexivity and symmetry are often bound together in equivalence
> relation. Reflexivity may be perceived primarily as a necessary part
> of equivalence. This seems to be the main reason why we thought so far
> that reflexivity on its own should be defined like the reflexivity
> part of ~ dfeqvrel3 below, i.e., by using the apparently self-evident
> ` x R x ` form.
> Another possible reason is that we are inclined to constrain ourselves
> to convenient special cases where the two forms are equivalent, e.g.
> the one with square Cartesian product:

> idinxpssinxp3 $p |- ( (_I i^i ( A X. A ) ) C_ ( R i^i ( A X. A ) )
> <-> (_I |` A ) C_ R ) and

> idinxpssinxp4 $p |- ( A. x e. A A. y e. A ( x = y -> x R y ) <-> A. x
> e. A x R x ) .
>
> Old reflexivity versions in set.mm or in a Mathbox now, with ` x R x `:
> df-reflexive $a |- ( R Reflexive A <-> ( R C_ ( A X. A ) /\ A. x e. A x R x ) )

> issref $p |- ( (_I |` A ) C_ R <-> A. x e. A x R x )

>
> Equivalence relations (new, suggested for set.mm, but other math
> sources seem to define it in a way which is similar to this one):
> df-eqvrels $a |- EqvRels = ( ( RefRels i^i SymRels ) i^i TrRels )
> which gives

> dfeqvrel2 $p |- ( EqvRel R <-> ( ( (_I |` dom R ) C_ R /\ `' R C_ R

> or Definition 35, [Suppes] p. 83., cf.https://oeis.org/A000110 ) is

[Mázsa Péter]

Hi Jim,

Thank you for your very kind mail and help! For now it is optimized
only for ` verify proof * ` and ` verify markup */… ` of Metamath (and
you are right: I need quite a lot of theorems from the Mathboxes of
other community members in the main part of set.mm, these are the
markup failures), I just wanted to have some gut feelings and the
widest possible collective wisdom about the whole enterprise at
first:)

Peter

> --
> 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/a6e056df-2e1b-0506-9c67-77d26bb5ecbc%40panix.com.
>

[Thierry Arnoux]

Hi Péter,

FYI, a discussion is going on the GitHub pull request Jim opened for
you, you might want to check it out:

https://github.com/metamath/set.mm/pull/2435

Do you have a GitHub account? Would you be able to participate there?

BR,
_
Thierry

[Mázsa Péter]

Hi Thierry, thank you for the information: I have a Github account and
I´ll participate there ASAP today. Thank you: Peter