Description: If A is an ideal of sets (a nonempty collection closed under subset and binary union) of the set D of finite bags (the primary applications being A = Fin and A = ~P B for some B ), then the set of all power series whose coefficient functions are supported on an element of A is a subgroup of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015) (Revised by AV, 16-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mplsubglem.s | |
|
mplsubglem.b | |
||
mplsubglem.z | |
||
mplsubglem.d | |
||
mplsubglem.i | |
||
mplsubglem.0 | |
||
mplsubglem.a | |
||
mplsubglem.y | |
||
mplsubglem.u | |
||
mplsubglem.r | |
||
Assertion | mplsubglem | |