measurableSet_biInter — Mathlib

English

If s is finite, the finite intersection over b ∈ s of f(b) is measurable provided each f(b) is measurable.

Русский

Если s конечно, пересечение по b из s множеств f(b) измеримо при условии, что каждое f(b) измеримо.

LaTeX

$$$[s.Finite] (\forall b \in s, \MeasurableSet (f(b))) \Rightarrow \MeasurableSet\left(\bigcap_{b \in s} f(b)\right)$$$

Lean4

theorem measurableSet_biInter {f : β → Set α} {s : Set β} (hs : s.Finite) (h : ∀ b ∈ s, MeasurableSet (f b)) :
    MeasurableSet (⋂ b ∈ s, f b) :=
  .biInter hs.countable h

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