biUnion_of_finite — Mathlib

English

If t is finite and each s_i is Carathéodory-measurable, then the union over i ∈ t is Carathéodory-measurable.

Русский

Если t конечное множество индексов и для каждого i ∈ t множество s_i карatheодory-измеримо, то объединение ∪_{i∈t} s_i карatheодory-измеримо.

LaTeX

$$t.Finite → (∀ i ∈ t, m.IsCaratheodory (s i)) → m.IsCaratheodory (⋃ i ∈ t, s i)$$

Lean4

theorem biUnion_of_finite {ι : Type*} {s : ι → Set α} {t : Set ι} (ht : t.Finite)
    (h : ∀ i ∈ t, m.IsCaratheodory (s i)) : m.IsCaratheodory (⋃ i ∈ t, s i) := by
  classical
  lift t to Finset ι using ht
  induction t using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    simp only [Finset.mem_coe, Finset.mem_insert, iUnion_iUnion_eq_or_left] at h ⊢
    exact m.isCaratheodory_union (h _ <| Or.inl rfl) (IH fun _ hj ↦ h _ <| Or.inr hj)

Похожие утверждения