measurableSet_sInter — Mathlib

English

Let S be a finite collection of subsets of α. If every member of S is measurable, then the intersection over all members of S is measurable.

Русский

Пусть S — конечная коллекция подмножеств α. Если каждый член S измерим, то пересечение всех членов S измеримо.

LaTeX

$$$|s| < \infty \rightarrow (\forall t \in s, \mathrm{MeasurableSet}(t)) \rightarrow \mathrm{MeasurableSet}\Big(\bigcap_{t \in s} t\Big)$$$

Lean4

theorem measurableSet_sInter {s : Set (Set α)} (hs : s.Finite) (h : ∀ t ∈ s, MeasurableSet t) : MeasurableSet (⋂₀ s) :=
  MeasurableSet.sInter hs.countable h

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