Description: The domain of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 19-Feb-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | dmmeas | ⊢ ( 𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isrnmeas | ⊢ ( 𝑀 ∈ ∪ ran measures → ( dom 𝑀 ∈ ∪ ran sigAlgebra ∧ ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) ) ) | |
2 | 1 | simpld | ⊢ ( 𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra ) |