iUnion — Mathlib

English

If each s_i is μ-null measurable for i in a countable index, then the union ⋃i s_i is μ-null measurable.

Русский

Если каждая s_i μ-нулеизмерима для i в счетном индексе, то объединение ⋃i s_i μ-нулеизмеримо.

LaTeX

$$[Countable ι] (∀ i, NullMeasurableSet (s i) μ) ⇒ NullMeasurableSet (⋃ i, s i) μ$$

Lean4

@[measurability]
protected theorem iUnion {ι : Sort*} [Countable ι] {s : ι → Set α} (h : ∀ i, NullMeasurableSet (s i) μ) :
    NullMeasurableSet (⋃ i, s i) μ :=
  MeasurableSet.iUnion h

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