Description: The volume of a measurable set is the same as its outer volume. (Contributed by Mario Carneiro, 17-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | mblvol | ⊢ ( 𝐴 ∈ dom vol → ( vol ‘ 𝐴 ) = ( vol* ‘ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | volres | ⊢ vol = ( vol* ↾ dom vol ) | |
2 | 1 | fveq1i | ⊢ ( vol ‘ 𝐴 ) = ( ( vol* ↾ dom vol ) ‘ 𝐴 ) |
3 | fvres | ⊢ ( 𝐴 ∈ dom vol → ( ( vol* ↾ dom vol ) ‘ 𝐴 ) = ( vol* ‘ 𝐴 ) ) | |
4 | 2 3 | eqtrid | ⊢ ( 𝐴 ∈ dom vol → ( vol ‘ 𝐴 ) = ( vol* ‘ 𝐴 ) ) |