measurable_generateFrom — Mathlib

English

Pullback of generateFrom equals generateFrom of preimages of the generator.

Русский

Обратное отображение generateFrom равно generateFrom предобразов генератора.

LaTeX

$$$$ \mathrm{comap} f (\mathrm{generateFrom} s) = \mathrm{generateFrom} (\mathrm{preimage} f \' ' s) $$$$

Lean4

theorem measurable_generateFrom [MeasurableSpace α] {s : Set (Set β)} {f : α → β}
    (h : ∀ t ∈ s, MeasurableSet (f ⁻¹' t)) : @Measurable _ _ _ (generateFrom s) f :=
  Measurable.of_le_map <| generateFrom_le h

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