measurableSet_blimsup — Mathlib

English

If each s_n is measurable whenever p(n) holds, then the blimsup of s with respect to atTop is measurable.

Русский

Если каждый s_n измерим тогда и только тогда, когда выполняется p(n), то блимcуп последовательности s по atTop измерим.

LaTeX

$$$\\forall s: \\mathbb{N} \\to \\mathrm{Set}\\,\\alpha\\,\\forall p: \\mathbb{N} \\to \\mathrm{Prop},\\ (\\forall n\\, p(n) \\to \\mathrm{MeasurableSet}(s(n))) \\Rightarrow \\mathrm{MeasurableSet}(\\mathrm{blimsup}(s, \\mathrm{atTop}, p))$$$

Lean4

@[measurability]
theorem measurableSet_blimsup {s : ℕ → Set α} {p : ℕ → Prop} (h : ∀ n, p n → MeasurableSet (s n)) :
    MeasurableSet <| blimsup s atTop p :=
  by
  simp only [blimsup_eq_iInf_biSup_of_nat, iSup_eq_iUnion, iInf_eq_iInter]
  exact .iInter fun _ => .iUnion fun m => .iUnion fun hm => h m hm.1

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