biUnion — Mathlib

English

Let f: ι → Set α and s ⊆ ι be countable. If every b ∈ s satisfies NullMeasurableSet (f(b)) μ, then NullMeasurableSet (⋃ b ∈ s, f(b)) μ.

Русский

Пусть f: ι → Set α и s ⊆ ι счетно. Если каждый b ∈ s удовлетворяет NullMeasurableSet (f(b)) μ, тогда NullMeasurableSet (⋃ b ∈ s, f(b)) μ.

LaTeX

$$s.Countable → (∀ b ∈ s, NullMeasurableSet (f b) μ) → NullMeasurableSet (⋃ b ∈ s, f b) μ$$

Lean4

protected theorem biUnion {f : ι → Set α} {s : Set ι} (hs : s.Countable) (h : ∀ b ∈ s, NullMeasurableSet (f b) μ) :
    NullMeasurableSet (⋃ b ∈ s, f b) μ :=
  MeasurableSet.biUnion hs h

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