biUnion — Mathlib

English

If t is countable, and every s i with i ∈ t is BaireMeasurableSet, then the union over i ∈ t is BaireMeasurableSet.

Русский

Если множитель t счётен и каждый s i для i ∈ t является Баирово измеримым, то объединение по i ∈ t тоже Баирово измеримо.

LaTeX

$$$$ \forall ι, {s : ι \to Set α}, {t : \text{Set } ι}, (ht : t.Countable) (h : \forall i \in t, \mathrm{BaireMeasurableSet}(s(i))) \Rightarrow \mathrm{BaireMeasurableSet}(\bigcup_{i \in t} s(i)). $$$$

Lean4

theorem biUnion {ι : Type*} {s : ι → Set α} {t : Set ι} (ht : t.Countable) (h : ∀ i ∈ t, BaireMeasurableSet (s i)) :
    BaireMeasurableSet (⋃ i ∈ t, s i) :=
  MeasurableSet.biUnion ht h

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