of_discrete

Mathlib.MeasureTheory.MeasurableSpace.Defs

URI: https://scilib.ai/kg/mathlib#Measurable.of_discrete

English

If α has a discrete measurable space, then any function f: α → β is measurable.

Русский

Если домен имеет дискретное пространство измеримости, то любая функция из α в β измерима.

LaTeX

$$$\\forall f:\\alpha \\to \\beta,\\text{ Measurable}_{\\text{Discrete}}(f).$$$

Lean4

@[measurability, fun_prop]
theorem of_discrete : Measurable f := fun _ _ ↦ .of_discrete

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru