Metamath Proof Explorer

Theorem measfn

Description: A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017)

Ref Expression
Assertion measfn ⊢ M ∈ measures ⁡ S → M Fn S

Proof

Step Hyp Ref Expression
1 measfrge0 ⊢ M ∈ measures ⁡ S → M : S ⟶ 0 +∞
2 1 ffnd ⊢ M ∈ measures ⁡ S → M Fn S