measurable

Mathlib.MeasureTheory.MeasurableSpace.Basic

URI: https://scilib.ai/kg/mathlib#Subsingleton.measurable

English

If α is a subsingleton, any f is measurable.

Русский

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

LaTeX

$$$$ \text{Measurable}(f) $$$$

Lean4

@[nontriviality, measurability]
theorem measurable [Subsingleton α] : Measurable f := fun _ _ => @Subsingleton.measurableSet α _ _ _

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

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

Разделы

Аффилиация

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