English
Let α be a measurable space. Let ι be a directed index set with atTop countably generated. If (s_i) is a monotone increasing family of subsets of α and there are frequently indices i with s_i measurable, then the union ⋃_i s_i is measurable.
Русский
Пусть α — измеримое пространство. Пусть ι — направленный индексный множитель с фильтром atTop, счетно порожденный. Если (s_i) — монотонно возрастающая семейство подмножеств α и часто встречаются индексы i такие, что s_i измеримы, тогда объединение ⋃_i s_i измеримо.
LaTeX
$$$$\\text{MeasurableSet}\\left(\\bigcup_{i} s_i\\right) \\quad\\text{if } \\text{Monotone}(s) \\text{ and } \\exists^\\infty i\\in atTop:\\, \\text{MeasurableSet}(s_i).$$$$
Lean4
protected theorem iUnion_of_monotone_of_frequently {ι : Type*} [Preorder ι] [(atTop : Filter ι).IsCountablyGenerated]
{s : ι → Set α} (hsm : Monotone s) (hs : ∃ᶠ i in atTop, MeasurableSet (s i)) : MeasurableSet (⋃ i, s i) :=
by
rcases exists_seq_forall_of_frequently hs with ⟨x, hx, hxm⟩
rw [← hsm.iUnion_comp_tendsto_atTop hx]
exact .iUnion hxm
