iInter — Mathlib

English

Countable intersection of measurable sets is measurable.

Русский

Счётное пересечение измеримых множеств измеримо.

LaTeX

$$$[Countable\ ι] \; (f : ι \to \text{Set } \alpha) \; (\forall b, \MeasurableSet(f(b))) \Rightarrow \MeasurableSet\left(\bigcap_{b} f(b)\right)$$$

Lean4

@[measurability]
theorem iInter [Countable ι] {f : ι → Set α} (h : ∀ b, MeasurableSet (f b)) : MeasurableSet (⋂ b, f b) :=
  .of_compl <| by rw [compl_iInter]; exact .iUnion fun b => (h b).compl

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