English
Let α be a measurable space. Let ι be a directed index with atTop countably generated. If s: ι → Set α is monotone and every s(i) is measurable, then the union ⋃_i s_i is measurable.
Русский
Пусть α — измеримое пространство. Пусть ι — направленный индекс с atTop счетно порожденным. При условии, что s(i) возрастает и каждый s(i) измерим, объединение ⋃_i s_i измеримо.
LaTeX
$$$$\\text{Monotone}(s) \\; \\land\\; \\forall i, \\text{MeasurableSet}(s_i) \\;\Longrightarrow\; \\text{MeasurableSet}\\left(\\bigcup_{i} s_i\\right).$$$$
Lean4
protected theorem iUnion_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)]
[(atTop : Filter ι).IsCountablyGenerated] {s : ι → Set α} (hsm : Monotone s) (hs : ∀ i, MeasurableSet (s i)) :
MeasurableSet (⋃ i, s i) := by
cases isEmpty_or_nonempty ι with
| inl _ => simp
| inr _ => exact .iUnion_of_monotone_of_frequently hsm <| .of_forall hs
