Theorem vonxrcl

Description: The Lebesgue measure of a set is an extended real. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonxrcl.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	vonxrcl.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
	vonxrcl.a	$$⊢\phi \to A\in S$$
Assertion	vonxrcl	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(A\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		vonxrcl.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		vonxrcl.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
3		vonxrcl.a	$$⊢\phi \to A\in S$$
4		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
5	1 2 3	voncl	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$
6	4 5	sselid	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(A\right)\in {ℝ}^{*}$$