nullMeasurableSet_biInter — Mathlib

English

If s is finite and every b in s has a null-measurable set f(b), then the finite intersection over 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_.Set.Finite.nullMeasurableSet_biInter {f : ι → Set α} {s : Set ι} (hs : s.Finite)
    (h : ∀ b ∈ s, NullMeasurableSet (f b) μ) : NullMeasurableSet (⋂ b ∈ s, f b) μ :=
  Finite.measurableSet_biInter hs h

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