Description: A measurable region is a subset of RR X. RR . (Contributed by Mario Carneiro, 21-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | areass | ⊢ ( 𝑆 ∈ dom area → 𝑆 ⊆ ( ℝ × ℝ ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmarea | ⊢ ( 𝑆 ∈ dom area ↔ ( 𝑆 ⊆ ( ℝ × ℝ ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑆 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) ) | |
2 | 1 | simp1bi | ⊢ ( 𝑆 ∈ dom area → 𝑆 ⊆ ( ℝ × ℝ ) ) |