Skip to content

Commit

Permalink
Renaming: MembEr -> CoMembEr
Browse files Browse the repository at this point in the history
  • Loading branch information
@mazsa
mazsa committed Jan 3, 2025
1 parent f144e55 commit ae393fe
Showing 1 changed file with 39 additions and 36 deletions.
75 changes: 39 additions & 36 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -450801,12 +450801,12 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
htmldef "ErALTV" as ' ErALTV ';
althtmldef "ErALTV" as ' ErALTV ';
latexdef "ErALTV" as "\mathrm{ErALTV}";
htmldef "MembErs" as ' MembErs ';
althtmldef "MembErs" as ' MembErs ';
latexdef "MembErs" as "\mathrm{MembErs}";
htmldef "MembEr" as ' MembEr ';
althtmldef "MembEr" as ' MembEr ';
latexdef "MembEr" as "\mathrm{MembEr}";
htmldef "CoMembErs" as ' CoMembErs ';
althtmldef "CoMembErs" as ' CoMembErs ';
latexdef "CoMembErs" as "\mathrm{CoMembErs}";
htmldef "CoMembEr" as ' CoMembEr ';
althtmldef "CoMembEr" as ' CoMembEr ';
latexdef "CoMembEr" as "\mathrm{CoMembEr}";
htmldef "Funss" as ' Funss ';
althtmldef "Funss" as ' Funss ';
latexdef "Funss" as "\mathrm{Funss}";
Expand Down Expand Up @@ -580791,8 +580791,8 @@ A collection of theorems for commuting equalities (or
quotients $)
$c ErALTV $. $( Equivalence relation on its domain quotient predicate $)

$c MembErs $. $( The class of membership equivalence relations $)
$c MembEr $. $( Membership equivalence relation predicate $)
$c CoMembErs $. $( The class of comembership equivalence relations $)
$c CoMembEr $. $( Comembership equivalence relation predicate $)

$c Funss $. $( The class of all function sets (used only once) $)
$c FunsALTV $. $( The class of functions, i.e., function relations $)
Expand Down Expand Up @@ -580907,14 +580907,14 @@ A collection of theorems for commuting equalities (or
domain quotient ` A ` .) $)
werALTV $a wff R ErALTV A $.

$( Extend the definition of a class to include the membership equivalence
$( Extend the definition of a class to include the comembership equivalence
relations class. $)
cmembers $a class MembErs $.
$( Extend the definition of a wff to include the membership equivalence
relation predicate. (Read: the membership equivalence relation on ` A ` ,
or, the restricted elementhood equivalence relation on its domain quotient
` A ` .) $)
wmember $a wff MembEr A $.
ccomembers $a class CoMembErs $.
$( Extend the definition of a wff to include the comembership equivalence
relation predicate. (Read: the comembership equivalence relation on
` A ` , or, the restricted coelement equivalence relation on its domain
quotient ` A ` .) $)
wcomember $a wff CoMembEr A $.

$( Extend the definition of a class to include the function set class. $)
cfunss $a class Funss $.
Expand Down Expand Up @@ -585491,21 +585491,21 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation.
~ brerser . (Contributed by Peter Mazsa, 12-Aug-2021.) $)
df-erALTV $a |- ( R ErALTV A <-> ( EqvRel R /\ R DomainQs A ) ) $.

$( Define the class of membership equivalence relations on their domain
$( Define the class of comembership equivalence relations on their domain
quotients. (Contributed by Peter Mazsa, 28-Nov-2022.) (Revised by Peter
Mazsa, 24-Jul-2023.) $)
df-members $a |- MembErs = { a | ,~ ( `' _E |` a ) Ers a } $.
df-comembers $a |- CoMembErs = { a | ,~ ( `' _E |` a ) Ers a } $.

$( Define the membership equivalence relation on the class ` A ` (or, the
restricted elementhood equivalence relation on its domain quotient
` A ` .) Alternate definitions are ~ dfmember2 and ~ dfmember3 .
$( Define the comembership equivalence relation on the class ` A ` (or, the
restricted coelement equivalence relation on its domain quotient ` A ` .)
Alternate definitions are ~ dfcomember2 and ~ dfcomember3 .

Later on, in an application of set theory I make a distinction between the
default elementhood concept and a special membership concept: membership
equivalence relation will be an integral part of that membership concept.
(Contributed by Peter Mazsa, 26-Jun-2021.) (Revised by Peter Mazsa,
28-Nov-2022.) $)
df-member $a |- ( MembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) $.
df-comember $a |- ( CoMembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) $.

$( Binary equivalence relation with natural domain, see the comment of
~ df-ers . (Contributed by Peter Mazsa, 23-Jul-2021.) $)
Expand Down Expand Up @@ -585544,22 +585544,25 @@ reflexive relation (see ~ dfrefrel3 ) in equivalence relation.

$( Alternate definition of the membership equivalence relation. (Contributed
by Peter Mazsa, 28-Nov-2022.) $)
dfmember $p |- ( MembEr A <-> ~ A ErALTV A ) $=
( wmember cep ccnv cres werALTV ccoels df-member df-coels erALTVeq1i bitr4i
ccoss ) ABACDAELZFAAGZFAHANMAIJK $.

$( Alternate definition of the membership equivalence relation. (Contributed
by Peter Mazsa, 25-Sep-2021.) $)
dfmember2 $p |- ( MembEr A <-> ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) ) $=
( wmember ccoels werALTV weqvrel cdm cqs wceq wa dfmember dferALTV2 bitri )
ABAACZDMEMFMGAHIAJAMKL $.
dfcomember $p |- ( CoMembEr A <-> ~ A ErALTV A ) $=
( wcomember ccnv cres werALTV ccoels df-comember df-coels erALTVeq1i bitr4i
cep ccoss ) ABAKCADLZEAAFZEAGANMAHIJ $.

$( Alternate definition of the membership equivalence relation. (Contributed
by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa, 17-Jul-2023.) $)
dfmember3 $p |- ( MembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) $=
( wmember ccoels weqvrel cdm cqs wceq wa wcoeleqvrel dfmember2 dfcoeleqvrel
cuni bicomi dmqscoelseq anbi12i bitri ) ABACZDZQEQFAGZHAIZALQFAGZHAJRTSUATR
AKMANOP $.
$( Alternate definition of the comembership equivalence relation.
(Contributed by Peter Mazsa, 25-Sep-2021.) $)
dfcomember2 $p |- ( CoMembEr A <->
( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) ) $=
( wcomember ccoels werALTV weqvrel cdm cqs wceq dfcomember dferALTV2 bitri
wa ) ABAACZDMEMFMGAHLAIAMJK $.

$( Alternate definition of the comembership equivalence relation.
(Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter Mazsa,
17-Jul-2023.) $)
dfcomember3 $p |- ( CoMembEr A <->
( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) $=
( wcomember ccoels weqvrel cdm wceq wa wcoeleqvrel dfcomember2 dfcoeleqvrel
cqs cuni bicomi dmqscoelseq anbi12i bitri ) ABACZDZQEQKAFZGAHZALQKAFZGAIRTS
UATRAJMANOP $.

$( Two ways to express membership equivalence relation on its domain
quotient. (Contributed by Peter Mazsa, 26-Sep-2021.) (Revised by Peter
Expand Down

0 comments on commit ae393fe

Please sign in to comment.