English
For a sequence s : ℕ → Set α, if each s i is Carathéodory and the family is pairwise disjoint, then for all n, sum over i < n of m(t ∩ s i) equals m(t ∩ ⋃ i < n, s i).
Русский
Для последовательности s: ℕ → Set α, если каждый s i карatheodory, и множества раздельны, то для каждого n выполняется равенство суммы по i < n: ∑ m(t ∩ s i) = m(t ∩ ⋃_{i < n} s i).
LaTeX
$$∀ {n}, (∑ i ∈ Finset.range n, m (t ∩ s i)) = m (t ∩ ⋃ i < n, s i)$$
Lean4
theorem isCaratheodory_sum {s : ℕ → Set α} (h : ∀ i, IsCaratheodory m (s i)) (hd : Pairwise (Disjoint on s))
{t : Set α} : ∀ {n}, (∑ i ∈ Finset.range n, m (t ∩ s i)) = m (t ∩ ⋃ i < n, s i)
| 0 => by simp
| Nat.succ n =>
by
rw [biUnion_lt_succ, Finset.sum_range_succ, Set.union_comm, isCaratheodory_sum h hd, m.measure_inter_union _ (h n),
add_comm]
intro a
simpa using fun (h₁ : a ∈ s n) i (hi : i < n) h₂ => (hd (ne_of_gt hi)).le_bot ⟨h₁, h₂⟩
