Theorem volsn

Description: A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	volsn	$$⊢A\in ℝ\to vol\left(\left\{A\right\}\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		snmbl	$$⊢A\in ℝ\to \left\{A\right\}\in \mathrm{dom}vol$$
2		mblvol	$$⊢\left\{A\right\}\in \mathrm{dom}vol\to vol\left(\left\{A\right\}\right)={vol}^{*}\left(\left\{A\right\}\right)$$
3	1 2	syl	$$⊢A\in ℝ\to vol\left(\left\{A\right\}\right)={vol}^{*}\left(\left\{A\right\}\right)$$
4		ovolsn	$$⊢A\in ℝ\to {vol}^{*}\left(\left\{A\right\}\right)=0$$
5	3 4	eqtrd	$$⊢A\in ℝ\to vol\left(\left\{A\right\}\right)=0$$