nullMeasurableSet_biInter — Mathlib

English

For a finite set s of indices, if each f(b) is null-measurable, then the intersection over b in s of f(b) is null-measurable.

Русский

Для конечного набора индексов s, если каждый f(b) нулево измерим, то пересечение по b из s является нулево измеримым.

LaTeX

$$$s\text{ finite} \Rightarrow (\forall b\in s, \mathrm{NullMeasurableSet}(f(b),\mu)) \Rightarrow \mathrm{NullMeasurableSet}(\bigcap_{b\in s} f(b),\mu).$$$

Lean4

theorem _root_.Finset.nullMeasurableSet_biInter {f : ι → Set α} (s : Finset ι)
    (h : ∀ b ∈ s, NullMeasurableSet (f b) μ) : NullMeasurableSet (⋂ b ∈ s, f b) μ :=
  s.finite_toSet.nullMeasurableSet_biInter h

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