Description: The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | voliunsge0.1 | ⊢ ( 𝜑 → 𝐸 : ℕ ⟶ dom vol ) | |
voliunsge0.2 | ⊢ ( 𝜑 → Disj 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) | ||
Assertion | voliunsge0 | ⊢ ( 𝜑 → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | voliunsge0.1 | ⊢ ( 𝜑 → 𝐸 : ℕ ⟶ dom vol ) | |
2 | voliunsge0.2 | ⊢ ( 𝜑 → Disj 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) | |
3 | eqid | ⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) | |
4 | eqid | ⊢ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) | |
5 | 3 4 1 2 | voliunsge0lem | ⊢ ( 𝜑 → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) |