disjointed — Mathlib

English

If each f(i) is measurable, then disjointed(f,n) is measurable for every n.

Русский

Если каждый f(i) измерим, то disjointed(f,n) измеримо для каждого n.

LaTeX

$$$\\forall i,\\ MeasurableSet(f(i)) \\Rightarrow \\forall n,\\ MeasurableSet(\\mathrm{disjointed}(f,n))$$$

Lean4

@[simp, measurability]
protected theorem disjointed {f : ℕ → Set α} (h : ∀ i, MeasurableSet (f i)) (n) : MeasurableSet (disjointed f n) :=
  disjointedRec (fun _ _ ht => MeasurableSet.diff ht <| h _) (h n)

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