measurableSet_bliminf — Mathlib

English

If each s_n is measurable, then the bliminf of s with respect to atTop is measurable.

Русский

Если каждый s_n измерим, то бллимиnф последовательности по 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{bliminf}(s, \\mathrm{atTop}, p))$$$

Lean4

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

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