Metamath Proof Explorer


Theorem mblvon

Description: The n-dimensional Lebesgue measure of a measurable set is the same as its n-dimensional Lebesgue outer measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses mblvon.1 φ X Fin
mblvon.2 φ A dom voln X
Assertion mblvon φ voln X A = voln* X A

Proof

Step Hyp Ref Expression
1 mblvon.1 φ X Fin
2 mblvon.2 φ A dom voln X
3 1 vonval φ voln X = voln* X CaraGen voln* X
4 3 fveq1d φ voln X A = voln* X CaraGen voln* X A
5 1 dmvon φ dom voln X = CaraGen voln* X
6 2 5 eleqtrd φ A CaraGen voln* X
7 fvres A CaraGen voln* X voln* X CaraGen voln* X A = voln* X A
8 6 7 syl φ voln* X CaraGen voln* X A = voln* X A
9 4 8 eqtrd φ voln X A = voln* X A