Hello all,
I've been dabbling with formalizing a result in clone theory, requiring me to
define the notion of a clone (which, so far as I know, is not already in
set.mm). One aspect of this is the notion of a projection: For a set A, a
natural number n > 0, and an integer 0 <= i < n, the i-th n-ary projection on A
is the function p : A^n \to A given by
p(x_0, ..., x_i, ..., x_{n-1}) = x_i.
I have tried to capture this notion in Metamath (in the general case), but I
would appreciate any feedback on my formulation, primarily with regards to
simplicity and conventions in set.mm. Below, I give an outline of my proposed
definition.
Firstly, I model the numbers n, i as ordinals for convenience; in particular,
the condition that 0 <= i < n simply becomes i e. n, while the condition that n
be positive is expressed as n e. ( _om \ 1o ).
Secondly, in desiring p to "pick out" the i-th argument, it appears to me that
defining p as a traditional n-ary operation, with domain A^n, is impractical
(correct me if I'm wrong). Instead, I've chosen to define p as a function on
length-n sequences of elements in A; in Metamath, we would have p : ( A ^m n )
--> A. Thus, for some sequence of arguments x e. ( A ^m n ), the i-th argument
would be given by ( x ` i ) for i e. n.
In total, I define a class proj which, when given a set A and suitable ordinals
n, i, returns the i-th n-ary projection on A. Here's the full definition:
|- proj = ( a e. _V |-> ( n e. ( _om \ 1o ) , i e. n |-> ( x e. ( a ^m n ) |->
( x ` i ) ) ) )
I'd like to ask: Is my approach reasonable, or have I gone off the rails?
I hope the above is sufficiently clear, and I thank any suggestions in advance.
All the best,
Adrian
--
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 visit
https://groups.google.com/d/msgid/metamath/174319635791.7.9068809461287120508.655573624%40passfwd.com.
