Theorem areass

Description: A measurable region is a subset of RR X. RR . (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	areass	$$⊢S\in \mathrm{dom}area\to S\subseteq {ℝ}^2$$

Proof

Step	Hyp	Ref	Expression
1		dmarea	$$⊢S\in \mathrm{dom}area\leftrightarrow \left(S\subseteq {ℝ}^2\wedge \forall x\in ℝS\left[\left\{x\right\}\right]\in {vol}^{-1}\left[ℝ\right]\wedge \left(x\in ℝ⟼vol\left(S\left[\left\{x\right\}\right]\right)\right)\in {𝐿}^1\right)$$
2	1	simp1bi	$$⊢S\in \mathrm{dom}area\to S\subseteq {ℝ}^2$$