generateFrom_measurableSet_of_generatePiSystem

English

For every g, if t ∈ generatePiSystem(g) then t is measurable in generateFrom g.

Русский

Для любого g, если t ∈ generatePiSystem(g), то t измеримо в generateFrom g.

LaTeX

$$$$ \forall g, \forall t \ (t \in \mathrm{generatePiSystem}(g) \Rightarrow \mathrm{MeasurableSet}_{\mathrm{generateFrom}(g)}(t)) $$$$

Lean4

theorem generateFrom_measurableSet_of_generatePiSystem {g : Set (Set α)} (t : Set α) (ht : t ∈ generatePiSystem g) :
    MeasurableSet[generateFrom g] t :=
  @generatePiSystem_measurableSet α (generateFrom g) g (fun _ h_s_in_g => measurableSet_generateFrom h_s_in_g) t ht

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