measurable_of_countable — Mathlib

English

If α is countable and every singleton in α is measurable, then any function f: α → β is measurable.

Русский

Если α счетно, и каждое множество вида {a} измеримо, то любая функция f: α → β измерима.

LaTeX

$$$[\\text{Countable } \\alpha] [\\text{MeasurableSingletonClass } \\alpha] (f : \\alpha \\to \\beta) : \\Measurable f$$$

Lean4

theorem measurable_of_countable [Countable α] [MeasurableSingletonClass α] (f : α → β) : Measurable f := fun s _ =>
  (f ⁻¹' s).to_countable.measurableSet

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