While I am working on theorems for matrices and polynomials, I have
increasing problems to find adequate class variables to formulate the
theorems appropriately. The available capital letters seem to be not
sufficient anymore. Therefore I would like to propose to add additional
class variables to set.mm.
In my latest pull request, I made already a proposal for such an extension:
$( Declare variable symbols that will be used to represent classes which
are
elements of a collection or of a base set of an extensible structure,
often having the same name. These variables should only be used for
sets
which are required in assumptions, i.e. either in antecedents, e.g.
` ( ( ph /\ .a. e. A ) -> ps ) ` , or in essential hypotheses
($e statements), e. g. ` $e |- ( ph -> .a. e. A ) $. ` . Another use
case for these variables is a situation in which variables are
substituted
by classes, e.g. on expanding definitions given as mappings:
` def $e |- I = ( p e. L |-> V ) $. ` and
` defval $p |- ( ( ph /\ .p. e. L ) -> ( I ` .p. ) = ... ` . As a
concrete example, see ~ mply1topmatval : In this example the class
variable ` P ` is already in use, so the new class variable ` .p. `
can be
used to substitue the set variable ` p ` used in the definition. $)
$v .a. $.
$v .b. $.
$v .c. $.
$v .m. $.
$v .p. $.
$( Let ` .a. ` be a class variable. $)
csA $f class .a. $.
$( Let ` .b. ` be a class variable. $)
csB $f class .b. $.
$( Let ` .c. ` be a class variable. $)
csC $f class .c. $.
$( Let ` .m. ` be a class variable. Usually used for representing a
matrix:
If ` A = ( N Mat R ) ` is the algebra of N x N matrices over (a ring)
` R ` and ` B = ( Base ` A ) ` is its base set (i.e. the set of all N
x N
matrices over ` R ` ), then ` .m. e. B ` is a special N x N matrix over
` R ` . $)
csM $f class .m. $.
$( Let ` .p. ` be a class variable. Usually used for representing a
polynomial: If ` P = ( Poly1 ` R ) ` is the algebra of (univariate)
polynomials over (a ring) ` R ` and ` B = ( Base ` P ) ` is its base
set
(i.e. the set of all univariate polynomials over ` R ` ), then
` .p. e. B ` is a special univariate polynomials over ` R ` . $)
csP $f class .p. $.
The two dots are taken from the approach for class variables representing
constants and operations (like .0. and .X. ), but also only one dot could
be used (e.g. .a analogous to .+ ).
Furthermore, I vacilate between using lower case or capital letters ( .a.
versus .A. ) - lower case letters suggest that the represented classes
should be sets, but capital letters make clear that these are variables for
classes.
I think the five additional variables should be enough for the moment
(actually I only need .m. and .p. for my current work).
Is there anybody else needing more class variables? How should they look
like? Is my proposal acceptable, or is one of the alternatives preferred?
If accepted, the 5 class variables could be moved from my Mathbox into the
main part (to the top of section "Class abstraction", where the other
variables are declared, or into sections of the topics for which they are
mainly used).
Alexander
--
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/78ed6c02-9526-4eca-b0af-82aa30af401b%40googlegroups.com.
