English
Let ι be a index set and m : ι → MeasurableSpace α. A subset s ⊆ α is measurable w.r.t. iSup m iff s lies in the σ-algebra generated by the collection { s ⊆ α | ∃ i, MeasurableSet[m i] s }.
Русский
Пусть ι — множество индексов и m : ι → MeasurableSpace α. Подмножество s ⊆ α измеримо по отношению к iSup m тогда и только тогда, когда s принадлежит σ‑алгебе, порождённой { s ⊆ α | ∃ i, MeasurableSet[m i] s }.
LaTeX
$$$\\text{MeasurableSet}_{\\,iSup\\;m}(s) \\iff s \\in \\sigma\\bigl\\{ t \\subseteq \\alpha \\;|\\; \\exists i, \\text{MeasurableSet}[m i]\, t \\bigr\\}.$$$
Lean4
theorem measurableSet_iSup {ι} {m : ι → MeasurableSpace α} {s : Set α} :
MeasurableSet[iSup m] s ↔ GenerateMeasurable {s : Set α | ∃ i, MeasurableSet[m i] s} s := by
simp only [iSup, measurableSet_sSup, exists_range_iff]
