measurableSet_generateFrom — Mathlib

English

If t is in the generating family s, then t is measurable with respect to the generated sigma-algebra generatedFrom s.

Русский

Если t принадлежит порождающей семье s, то t измеримо относительно порожденной сигма-алгебры GenerateFrom s.

LaTeX

$$$\\text{t} \\in s \\implies \\text{MeasurableSet}[\\text{generateFrom}(s)]\\,t$$$

Lean4

theorem measurableSet_generateFrom {s : Set (Set α)} {t : Set α} (ht : t ∈ s) : MeasurableSet[generateFrom s] t :=
  .basic t ht

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