measurable_to_countable' — Mathlib

English

If for every x in α, f^{-1}({x}) is measurable, then f is measurable.

Русский

Если для каждого x ∈ α множество f^{-1}({x}) измеримо, то функция f измерима.

LaTeX

$$$\\forall x,\\ MeasurableSet(f^{-1}\\{x\\}) \\Rightarrow Measurable f$$$

Lean4

theorem measurable_to_countable' [MeasurableSpace α] [Countable α] [MeasurableSpace β] {f : β → α}
    (h : ∀ x, MeasurableSet (f ⁻¹' { x })) : Measurable f :=
  measurable_to_countable fun y => h (f y)

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