iInter — Mathlib

English

If every f i is μ-null measurable for i in a countable index, then the intersection ⋂i f i is μ-null measurable.

Русский

Если каждый f(i) μ-нулеизмерим, индексы счетны, тогда пересечение ⋂i f(i) μ-нулеизмеримо.

LaTeX

$$[ι : Sort*] [Countable ι] (∀ i, NullMeasurableSet (f i) μ) → NullMeasurableSet (⋂ i, f i) μ$$

Lean4

@[measurability]
protected theorem iInter {ι : Sort*} [Countable ι] {f : ι → Set α} (h : ∀ i, NullMeasurableSet (f i) μ) :
    NullMeasurableSet (⋂ i, f i) μ :=
  MeasurableSet.iInter h

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