English
Let α be a measurable space and ι a directed index with atTop countably generated. If (s_i) is an antitone (decreasing) family of subsets of α and there are frequently i with s_i measurable, then the intersection ⋂_i s_i is measurable.
Русский
Пусть α — измеримое пространство и ι — направленный индекс с atTop, счетно порожденный. Если (s_i) — убывающая (антитонная) семействo подмножеств α и часто встречаются i с тем, что s_i измеримо, то пересечение ⋂_i s_i измеримо.
LaTeX
$$$$\\text{MeasurableSet}\\left(\\bigcap_{i} s_i\\right) \\quad\\text{if } \\text{Antitone}(s) \\text{ and } \\exists^\\infty i\\in atTop:\\, \\text{MeasurableSet}(s_i).$$$$
Lean4
protected theorem iInter_of_antitone_of_frequently {ι : Type*} [Preorder ι] [(atTop : Filter ι).IsCountablyGenerated]
{s : ι → Set α} (hsm : Antitone s) (hs : ∃ᶠ i in atTop, MeasurableSet (s i)) : MeasurableSet (⋂ i, s i) :=
by
rw [← compl_iff, compl_iInter]
exact .iUnion_of_monotone_of_frequently (compl_anti.comp hsm) <| hs.mono fun _ ↦ .compl
