sInter — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sInter {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, MeasurableSet t) : MeasurableSet (⋂₀ s) :=
  by
  rw [sInter_eq_biInter]
  exact MeasurableSet.biInter hs h

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