measurableSet_sup — Mathlib

English

Let α be a set equipped with two σ-algebras F and G. A subset s ⊆ α is measurable with respect to the join F ⊔ G if and only if s lies in the σ-algebra generated by the union of F and G.

Русский

Пусть α оснащено двумя σ‑алгебрами F и G. Подмножество s ⊆ α измеримо по отношению к объединению F ⊔ G тогда и только тогда, когда s принадлежит σ‑алгебе, порождённой объединением F ∪ G.

LaTeX

$$$\\text{MeasurableSet}_{F\\lor G}(s) \\iff s \\in \\sigma\\bigl(\\text{MeasurableSet}_{F} \\cup \\text{MeasurableSet}_{G}\\bigr).$$$

Lean4

theorem measurableSet_sup {m₁ m₂ : MeasurableSpace α} {s : Set α} :
    MeasurableSet[m₁ ⊔ m₂] s ↔ GenerateMeasurable (MeasurableSet[m₁] ∪ MeasurableSet[m₂]) s :=
  Iff.rfl

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