iUnion — Mathlib

English

Countable union of measurable sets is measurable.

Русский

Счётная объединение измеримых множеств измеримо.

LaTeX

$$$[Countable\ ι] \; \forall f : ι \to Set \alpha,\ (\forall b, MeasurableSet(f(b))) \Rightarrow MeasurableSet\left(\bigcup_{b} f(b)\right)$$$

Lean4

@[measurability]
protected theorem iUnion [Countable ι] ⦃f : ι → Set α⦄ (h : ∀ b, MeasurableSet (f b)) : MeasurableSet (⋃ b, f b) :=
  by
  cases isEmpty_or_nonempty ι
  · simp
  · rcases exists_surjective_nat ι with ⟨e, he⟩
    rw [← iUnion_congr_of_surjective _ he (fun _ => rfl)]
    exact m.measurableSet_iUnion _ fun _ => h _

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