English
For sets s1, s2, the real-valued measure of their union is at most the sum of their real-valued measures.
Русский
Для множеств s1, s2 выполнено μ.real(s1 ∪ s2) ≤ μ.real s1 + μ.real s2.
LaTeX
$$$ \\mu.real (s_{1} \\cup s_{2}) \\leq \\mu.real s_{1} + \\mu.real s_{2} $$$
Lean4
theorem measureReal_union_le (s₁ s₂ : Set α) : μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂ :=
by
rcases eq_top_or_lt_top (μ (s₁ ∪ s₂)) with h | h
· simp only [Measure.real, h, ENNReal.toReal_top]
exact add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
· have A : μ s₁ ≠ ∞ := measure_ne_top_of_subset subset_union_left h.ne
have B : μ s₂ ≠ ∞ := measure_ne_top_of_subset subset_union_right h.ne
simp only [Measure.real, ← ENNReal.toReal_add A B]
exact ENNReal.toReal_mono (by simp [A, B]) (measure_union_le _ _)
