biInter — Mathlib

English

Countable intersection over a subset t of indices of BaireMeasurableSet(s i) is BaireMeasurableSet.

Русский

Счётное пересечение по индексов из множества 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 biInter {ι : Type*} {s : ι → Set α} {t : Set ι} (ht : t.Countable) (h : ∀ i ∈ t, BaireMeasurableSet (s i)) :
    BaireMeasurableSet (⋂ i ∈ t, s i) :=
  MeasurableSet.biInter ht h

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