biUnion — Mathlib

English

If s is countable and each f(b) is measurable for b ∈ s, then the union over b ∈ s of f(b) is measurable.

Русский

Если s счётно, и для каждого b ∈ s множество f(b) измеримо, то объединение по b из s множеств f(b) измеримо.

LaTeX

$$$[s.Countable] \; (\forall b \in s, \MeasurableSet(f(b))) \Rightarrow \MeasurableSet(\bigcup_{b} f(b))$$$

Lean4

protected theorem biUnion {f : β → Set α} {s : Set β} (hs : s.Countable) (h : ∀ b ∈ s, MeasurableSet (f b)) :
    MeasurableSet (⋃ b ∈ s, f b) := by
  rw [biUnion_eq_iUnion]
  have := hs.to_subtype
  exact MeasurableSet.iUnion (by simpa using h)

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