Description: The measure of the union of countable sets is less than or equal to the sum of the measures, Property 112C (d) of Fremlin1 p. 16. (Contributed by Glauco Siliprandi, 17-Aug-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | meaiunle.nph | |- F/ n ph |
|
| meaiunle.m | |- ( ph -> M e. Meas ) |
||
| meaiunle.s | |- S = dom M |
||
| meaiunle.z | |- Z = ( ZZ>= ` N ) |
||
| meaiunle.e | |- ( ph -> E : Z --> S ) |
||
| Assertion | meaiunle | |- ( ph -> ( M ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( M ` ( E ` n ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | meaiunle.nph | |- F/ n ph |
|
| 2 | meaiunle.m | |- ( ph -> M e. Meas ) |
|
| 3 | meaiunle.s | |- S = dom M |
|
| 4 | meaiunle.z | |- Z = ( ZZ>= ` N ) |
|
| 5 | meaiunle.e | |- ( ph -> E : Z --> S ) |
|
| 6 | eqid | |- ( n e. Z |-> ( ( E ` n ) \ U_ x e. ( N ..^ n ) ( E ` x ) ) ) = ( n e. Z |-> ( ( E ` n ) \ U_ x e. ( N ..^ n ) ( E ` x ) ) ) |
|
| 7 | 1 2 3 4 5 6 | meaiunlelem | |- ( ph -> ( M ` U_ n e. Z ( E ` n ) ) <_ ( sum^ ` ( n e. Z |-> ( M ` ( E ` n ) ) ) ) ) |