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 ( 𝜑𝑋 ∈ Fin )
ovnsplit.a ( 𝜑𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
Assertion ovnsplit ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝐵 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnsplit.x ( 𝜑𝑋 ∈ Fin )
2 ovnsplit.a ( 𝜑𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
3 inundif ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐵 ) ) = 𝐴
4 3 eqcomi 𝐴 = ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐵 ) )
5 4 fveq2i ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ 𝑋 ) ‘ ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐵 ) ) )
6 5 a1i ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln* ‘ 𝑋 ) ‘ ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐵 ) ) ) )
7 2 ssinss1d ( 𝜑 → ( 𝐴𝐵 ) ⊆ ( ℝ ↑m 𝑋 ) )
8 2 ssdifssd ( 𝜑 → ( 𝐴𝐵 ) ⊆ ( ℝ ↑m 𝑋 ) )
9 1 7 8 ovnsubadd2 ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ( ( 𝐴𝐵 ) ∪ ( 𝐴𝐵 ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝐵 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝐵 ) ) ) )
10 6 9 eqbrtrd ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐴 ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝐵 ) ) +𝑒 ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝐵 ) ) ) )