English
Let α be a type and ms a set of σ-algebras on α. A subset s ⊆ α is measurable with respect to the supremum sSup ms if and only if s lies in the σ-algebra generated by the collection { s ⊆ α | ∃ m ∈ ms, MeasurableSet[m] s }.
Русский
Пусть α — множество, на котором задано множество σ‑алгебр ms. Подмножество s ⊆ α измеримо по отношению к верхней границе sSup ms тогда и только тогда, когда s принадлежит σ‑алгебе, порождённой коллекцией { s ⊆ α | существует m ∈ ms, MeasurableSet[m] s }.
LaTeX
$$$\\text{MeasurableSet}_{\\,sSup\\;\\mathcal{M}}(s) \\iff s \\in \\sigma\\bigl\\{ t \\subseteq \\alpha \\;|\\; \\exists m \\in \\mathcal{M}, \\text{MeasurableSet}[m]\, t \\bigr\\}.$$$
Lean4
theorem measurableSet_sSup {ms : Set (MeasurableSpace α)} {s : Set α} :
MeasurableSet[sSup ms] s ↔ GenerateMeasurable {s : Set α | ∃ m ∈ ms, MeasurableSet[m] s} s :=
by
change GenerateMeasurable (⋃₀ _) _ ↔ _
simp [← setOf_exists]
