On Tue, Sep 8, 2020 at 3:46 PM 'Stanislas Polu' via Metamath <
[email protected]> wrote:
> I was expecting to find something along the very broad lines of:
>
> ```
> ( CCfld gsum { { 1 , A } , { 1 , B } , { 1 , C } } ) = ( ( CCfld gsum
> { { 1 , A } , { 1 , B } } ) + ( CCfld gsum { { 1 , C } } ) )
> ```
>
Well, in the first place the statement is false, and a bit not well typed.
The right argument of gsum is a finitely supported function, which is a set
of ordered pairs, which means (1) you should use <. 1 , A >. for the
points, and (2) the domain values should be distinct or it's not a
function; that is, instead of { <. 1 , A >. , <. 1 , B >. , <. 1 , C >. }
you should have { <. 1 , A >. , <. 2 , B >. , <. 3 , C >. }.The easiest way
to construct finite functions on integers like this is using df-word, as in
<" A B C ">, and the relevant lemmas for manipulating such expressions are
gsumws1 and gsumccat, also specialized to gsumccatsn and gsumws2 (it might
be good to fill out the matrix here and prove gsumwsN for n = 3..8).
Mario
--
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/CAFXXJSudhyg1zSUqiTspDwgoGoQ5wmBYBPuRf_xHPmsrnjzYgA%40mail.gmail.com.
