sUnion — Mathlib

English

Let s be a countable collection of sets. If every t ∈ s is μ-null measurable, then the union of all t in s is μ-null measurable.

Русский

Пусть s — счетная коллекция множеств. Если каждое множество t из s μ-нулеизмеримо, то объединение всех t из s μ-нулеизмеримо.

LaTeX

$$∀ {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, NullMeasurableSet t μ), NullMeasurableSet (sUnion s) μ$$

Lean4

protected theorem sUnion {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, NullMeasurableSet t μ) :
    NullMeasurableSet (⋃₀ s) μ := by
  rw [sUnion_eq_biUnion]
  exact MeasurableSet.biUnion hs h

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