generateFrom_iUnion_measurableSet

English

For a family m: ι → MeasurableSpace α, the σ-algebra generated by the union of all measurable sets across m equals the supremum of the spaces: GenerateFrom (⋃ i, {t ⊆ α | MeasurableSet[m i] t}) = ⨆ i, m i.

Русский

Для семейства m: ι → MeasurableSpace α σ‑алгебa, порожденная объединением всех измеримых множеств по каждому m i, равна наибольшему верхнему пределу пространств: GenerateFrom(⋃ i, {t ⊆ α | MeasurableSet[m i] t}) = ⨆ i, m i.

LaTeX

$$$\\text{GenerateFrom}\\Bigl(\\bigcup_i \\{ t \\subseteq \\alpha \\;|\\; \\text{MeasurableSet}[m(i)]\\, t \\}\\Bigr) = \\bigvee_i m(i).$$$

Lean4

theorem generateFrom_iUnion_measurableSet (m : ι → MeasurableSpace α) :
    generateFrom (⋃ n, {t | MeasurableSet[m n] t}) = ⨆ n, m n :=
  (@giGenerateFrom α).l_iSup_u m

Похожие утверждения