This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovolsn

Description: A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014)

		Ref	Expression
	Assertion	ovolsn	$⊢ A \in ℝ \to {vol}^{*} (\{A\}) = 0$

Step	Hyp	Ref	Expression
1		snfi	$⊢ \{A\} \in Fin$
2		snssi	$⊢ A \in ℝ \to \{A\} \subseteq ℝ$
3		ovolfi	$⊢ (\{A\} \in Fin \land \{A\} \subseteq ℝ) \to {vol}^{*} (\{A\}) = 0$
4	1 2 3	sylancr	$⊢ A \in ℝ \to {vol}^{*} (\{A\}) = 0$