measurable_of_finite — Mathlib

English

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

Русский

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

LaTeX

$$$[Finite \\alpha] [MeasurableSingletonClass \\alpha] (f : \\alpha \\to \\beta) : \\Measurable f$$$

Lean4

theorem measurable_of_finite [Finite α] [MeasurableSingletonClass α] (f : α → β) : Measurable f :=
  measurable_of_countable f

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