biInter — Mathlib

English

Let f: β → Set α and s ⊆ β be countable. If every b ∈ s satisfies NullMeasurableSet (f b) μ, then NullMeasurableSet (⋂ b ∈ s, f b) μ.

Русский

Пусть f: β → Set α и s ⊆ β счетно. Если для каждого b ∈ s выполнено NullMeasurableSet (f b) μ, то NullMeasurableSet (⋂ b ∈ s, f b) μ.

LaTeX

$$s.Countable → (∀ b ∈ s, NullMeasurableSet (f b) μ) → NullMeasurableSet (⋂ b ∈ s, f b) μ$$

Lean4

protected theorem biInter {f : β → Set α} {s : Set β} (hs : s.Countable) (h : ∀ b ∈ s, NullMeasurableSet (f b) μ) :
    NullMeasurableSet (⋂ b ∈ s, f b) μ :=
  MeasurableSet.biInter hs h

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