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 | |- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | volres | |- vol = ( vol* |` dom vol ) |
|
2 | 1 | fveq1i | |- ( vol ` A ) = ( ( vol* |` dom vol ) ` A ) |
3 | fvres | |- ( A e. dom vol -> ( ( vol* |` dom vol ) ` A ) = ( vol* ` A ) ) |
|
4 | 2 3 | eqtrid | |- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) ) |