Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Basic measure theory
Measures
meaiunle
Metamath Proof Explorer
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
⊢ Ⅎ 𝑛 𝜑
meaiunle.m
⊢ ( 𝜑 → 𝑀 ∈ Meas )
meaiunle.s
⊢ 𝑆 = dom 𝑀
meaiunle.z
⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
meaiunle.e
⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑆 )
Assertion
meaiunle
⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
Proof
Step
Hyp
Ref
Expression
1
meaiunle.nph
⊢ Ⅎ 𝑛 𝜑
2
meaiunle.m
⊢ ( 𝜑 → 𝑀 ∈ Meas )
3
meaiunle.s
⊢ 𝑆 = dom 𝑀
4
meaiunle.z
⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
5
meaiunle.e
⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑆 )
6
eqid
⊢ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑥 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑥 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑥 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑥 ) ) )
7
1 2 3 4 5 6
meaiunlelem
⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )