Metamath Proof Explorer


Theorem ovnsplit

Description: The n-dimensional Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovnsplit.x φ X Fin
ovnsplit.a φ A X
Assertion ovnsplit φ voln* X A voln* X A B + 𝑒 voln* X A B

Proof

Step Hyp Ref Expression
1 ovnsplit.x φ X Fin
2 ovnsplit.a φ A X
3 inundif A B A B = A
4 3 eqcomi A = A B A B
5 4 fveq2i voln* X A = voln* X A B A B
6 5 a1i φ voln* X A = voln* X A B A B
7 2 ssinss1d φ A B X
8 2 ssdifssd φ A B X
9 1 7 8 ovnsubadd2 φ voln* X A B A B voln* X A B + 𝑒 voln* X A B
10 6 9 eqbrtrd φ voln* X A voln* X A B + 𝑒 voln* X A B