English
For a metric outer measure μ, the union of a finite family of pairwise separated sets has measure equal to the sum of the measures of the pieces.
Русский
Для метрической внешней меры μ объединение конечного числа попарно разделенных множеств имеет меру, равную сумме мер частей.
LaTeX
$$μ(⋃ i ∈ I, s i) = ∑ i ∈ I μ(s i) for pairwise separated s i.$$
Lean4
/-- A metric outer measure is additive on a finite set of pairwise metric separated sets. -/
theorem finset_iUnion_of_pairwise_separated (hm : IsMetric μ) {I : Finset ι} {s : ι → Set X}
(hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → Metric.AreSeparated (s i) (s j)) : μ (⋃ i ∈ I, s i) = ∑ i ∈ I, μ (s i) := by
classical
induction I using Finset.induction_on with
| empty => simp
| insert i I hiI ihI =>
simp only [Finset.mem_insert] at hI
rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]
exacts [fun i hi j hj hij => hI i (Or.inr hi) j (Or.inr hj) hij,
Metric.AreSeparated.finset_iUnion_right fun j hj =>
hI i (Or.inl rfl) j (Or.inr hj) (ne_of_mem_of_not_mem hj hiI).symm]
