disjointed — Mathlib

English

If each f(n) is NullMeasurable with respect to μ, then the disjointed sequence is NullMeasurable.

Русский

Если каждый f(n) — NullMeasurable относительно μ, то disjointed f n — NullMeasurable.

LaTeX

$$$\\forall n, \\text{NullMeasurableSet } (f\\, n) μ \\Rightarrow \\text{NullMeasurableSet } (\\text{disjointed } f\\, n) μ$$$

Lean4

@[simp]
protected theorem disjointed {f : ℕ → Set α} (h : ∀ i, NullMeasurableSet (f i) μ) (n) :
    NullMeasurableSet (disjointed f n) μ :=
  MeasurableSet.disjointed h n

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