I am trying to prove the weak compositions of integers by giving an explicit
isomorphism. https://en.wikipedia.org/wiki/Composition_(combinatorics)
In particular I want to prove theorem 2 of
https://en.wikipedia.org/wiki/Stars_and_bars_(combinatorics)
```
h1:: |- ( ph -> N e. NN )
h2:: |- ( ph -> K e. NN0 )
h3:: |- A = { a e. ~P ( 1 ... ( ( N - 1 ) + K ) ) | ( # ` a ) = N }
h4:: |- B = { f | ( f : ( 1 ... N ) --> NN0 /\ sum_ i e. ( 1 ... N ) (
f ` i ) = K ) }
h5:: |- F = ( x e. A |-> ( h e. ( 1 ... N ) |-> if ( h = N , ( ( (
N + K ) - 1 ) - sup ( x , RR , < ) ) , ( ( ( iota_ d e. x ( # ` { v e.
x | v <_ d } ) = ( h + 1 ) ) - ( iota_ e e. x ( # ` { w e. x | w <_
e } ) = h ) ) - 1 ) ) ) )
h6:: |- G = ( y e. B |-> { l e. ( 1 ... ( ( N - 1 ) + K ) ) | E. s e.
( 1 ... N ) l = ( sum_ t e. ( 1 ... s ) ( y ` t ) + ( s - 1 ) ) } )
qed:?: |- ( ( ph /\ X e. A ) -> ( F ` ( G ` X ) ) = X )
```
In particular I want to calculate the size of B. My idea was to use an explicit
isomorphism from A to B while there is a theorem that gives me the size of
A, namely https://us.metamath.org/mpeuni/hashbcval.html
I don't know if my definitions are the best or if there is a better way.
Alternatively I have tried to maybe use the isomorphism of the k-element
subsets of 1 to n to the ordered functions
of ( 1 ... N ) to ( 1 ... K ) where for a < b f(a) < f(b) and use that to show
that this is isomorphic to B.
There seems to be something that is likely nice to be used.
https://us.metamath.org/mpeuni/fz1iso.html
But I have not figured out a proof blueprint. Some similar lemmas exist but I
am not sure what the least painful way of doing things is.
My plan was to show that the strictly monotone increasing functions from ( 1
... K ) to ( 1 ... N ) are bijective onto the k-element subsets of ( 1 ... N )
The mapping g taking a function f onto the power set of ( 1 ... N ) is defined
by taking the range of f. I want to show that the function g is injective by
considering two f1, f2 and show that g(f1) is not equal to g(f2)
Surjectivity I want to show separately. Given a k-elemental subset x of ( 1 ...
N ) generate the order isomorphism with fz1iso and put it in the range function.
therefore let y be the order isomorphism of x and show that it is a monotonely
increasing function from ( 1 ... K ) to ( 1 ... N )
Is this plan sound? Because I seem to struggle with the existential quantor in
fz1iso.
________________________________________________________
Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe.
https://www.eclipso.eu
--
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/f47b1de5f2cb729b9e788db137eecf2e%40mail.eclipso.de.
