English
If for all i, s_i is Caratheodory-measurable and the family is pairwise disjoint, then ⋃ i, s_i is Carathéodory-measurable.
Русский
Если для всех i карatheodory-множества s_i и множество s_i попарно не перекрываются, то ⋃ i, s_i карatheodory-измеримо.
LaTeX
$$m.IsCaratheodory (⋃ i, s i)$$
Lean4
/-- Use `isCaratheodory_iUnion` instead, which does not require the disjoint assumption. -/
theorem isCaratheodory_iUnion_of_disjoint {s : ℕ → Set α} (h : ∀ i, IsCaratheodory m (s i))
(hd : Pairwise (Disjoint on s)) : IsCaratheodory m (⋃ i, s i) :=
by
apply (isCaratheodory_iff_le' m).mpr
intro t
have hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i < n, s i) :=
by
convert measure_iUnion_le (μ := m) fun i => t ∩ s i using 1
· simp [inter_iUnion]
· simp [ENNReal.tsum_eq_iSup_nat, isCaratheodory_sum m h hd]
grw [hp]
rw [ENNReal.iSup_add]
refine iSup_le fun n => le_trans (add_le_add_left ?_ _) (ge_of_eq (isCaratheodory_iUnion_lt m (fun i _ => h i) _))
refine m.mono (diff_subset_diff_right ?_)
exact iUnion₂_subset fun i _ => subset_iUnion _ i
