sInter — Mathlib

English

For a countable set of sets s, if every t ∈ s is μ-null measurable, then the intersection ⋂ t ∈ s t is μ-null measurable.

Русский

Для счетного множества множеств s, если каждое t ∈ s μ-нулеизмеримо, то пересечение ⋂ t∈s t μ-нулеизмеримо.

LaTeX

$$∀ {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, NullMeasurableSet t μ), NullMeasurableSet (sInter s) μ$$

Lean4

protected theorem sInter {s : Set (Set α)} (hs : s.Countable) (h : ∀ t ∈ s, NullMeasurableSet t μ) :
    NullMeasurableSet (⋂₀ s) μ :=
  MeasurableSet.sInter hs h

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