English
Let α be a measurable space. Let ι be a directed index and s: ι → Set α be Antitone (decreasing). If hs : ∃ᶠ i in atTop, MeasurableSet (s i), then MeasurableSet (⋂ i, s i).
Русский
Пусть α — измеримое пространство. Пусть ι — направленный индекс, и s: ι → Set α убывающая. Если встречаются часто измеримые множества s_i, то пересечение ⋂_i s_i измеримо.
LaTeX
$$$$\\text{Antitone}(s) \\land \\exists^\\infty i\\in atTop:\\, \\text{MeasurableSet}(s_i) \\;\Longrightarrow\\; \\text{MeasurableSet}\\left(\\bigcap_{i} s_i\\right).$$$$
Lean4
protected theorem iInter_of_antitone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)]
[(atTop : Filter ι).IsCountablyGenerated] {s : ι → Set α} (hsm : Antitone s) (hs : ∀ i, MeasurableSet (s i)) :
MeasurableSet (⋂ i, s i) := by
rw [← compl_iff, compl_iInter]
exact .iUnion_of_monotone (compl_anti.comp hsm) fun i ↦ (hs i).compl
