generate_has_subset_generate_measurable

English

If s belongs to generate(C), then s is measurable with respect to generateFrom(C).

Русский

Если s ∈ generate(C), то s измерима относительно generateFrom(C).

LaTeX

$$$ s \in \ generate(C) \Rightarrow s \in \text{MeasurableSet}_{\operatorname{generateFrom}(C)}(s). $$$

Lean4

theorem generate_has_subset_generate_measurable {C : Set (Set α)} {s : Set α} (hs : (generate C).Has s) :
    MeasurableSet[generateFrom C] s :=
  generate_le (ofMeasurableSpace (generateFrom C)) (fun _ => measurableSet_generateFrom) s hs

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