measurableSet_biInter — Mathlib

English

If s is a finite set of indices, and each f(b) is measurable for b ∈ s, then the intersection over b in s of f(b) is measurable.

Русский

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

LaTeX

$$$\text{Finset}(s).measurableSet\_biInter$$$

Lean4

theorem measurableSet_biInter {f : β → Set α} (s : Finset β) (h : ∀ b ∈ s, MeasurableSet (f b)) :
    MeasurableSet (⋂ b ∈ s, f b) :=
  s.finite_toSet.measurableSet_biInter h

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