nullMeasurableSet_sInter — Mathlib

English

If s is finite and every t in s is null-measurable, then the sInter (intersection over s) is null-measurable.

Русский

Если s конечно и каждый элемент s нулево измерим, то пересечение по s нулево измеримо.

LaTeX

$$$s\text{ finite} \Rightarrow (\forall t\in s, \mathrm{NullMeasurableSet}(t,\mu)) \Rightarrow \mathrm{NullMeasurableSet}(\bigcap s,\mu).$$$

Lean4

theorem _root_.Set.Finite.nullMeasurableSet_sInter {s : Set (Set α)} (hs : s.Finite)
    (h : ∀ t ∈ s, NullMeasurableSet t μ) : NullMeasurableSet (⋂₀ s) μ :=
  NullMeasurableSet.sInter (Finite.countable hs) h

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