Theorem measvxrge0

Description: The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016)

	Ref	Expression
Assertion	measvxrge0	$$⊢\left(M\in \mathrm{measures}\left(S\right)\wedge A\in S\right)\to M\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$

Proof

Step	Hyp	Ref	Expression
1		measfrge0	$$⊢M\in \mathrm{measures}\left(S\right)\to M:S⟶\left[0,\mathrm{+\infty }\right]$$
2	1	ffvelcdmda	$$⊢\left(M\in \mathrm{measures}\left(S\right)\wedge A\in S\right)\to M\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$