measurableSet_limsup — Mathlib

English

If every s_n is measurable, then the limsup of s with atTop is measurable.

Русский

Если каждый s_n измерим, то предел верхний (limsup) последовательности измерим.

LaTeX

$$$\\forall s: \\mathbb{N} \\to \\mathrm{Set}\\,\\alpha,\\ (\\forall n, \\mathrm{MeasurableSet}(s(n))) \\Rightarrow \\mathrm{MeasurableSet}(\\mathrm{Filter.limsup}(s, \\mathrm{atTop}))$$$

Lean4

@[measurability]
theorem measurableSet_limsup {s : ℕ → Set α} (hs : ∀ n, MeasurableSet <| s n) :
    MeasurableSet <| Filter.limsup s Filter.atTop := by
  simpa only [← blimsup_true] using measurableSet_blimsup fun n _ => hs n

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