biInter — Mathlib

English

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

Русский

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

LaTeX

$$$[s.Countable] \; (\forall b \in s, \MeasurableSet (f(b))) \Rightarrow \MeasurableSet\left(\bigwedge_{b \in s} f(b)\right)$$$

Lean4

theorem biInter {f : β → Set α} {s : Set β} (hs : s.Countable) (h : ∀ b ∈ s, MeasurableSet (f b)) :
    MeasurableSet (⋂ b ∈ s, f b) :=
  .of_compl <| by rw [compl_iInter₂]; exact .biUnion hs fun b hb => (h b hb).compl

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