measurable_of_subsingleton_codomain

Mathlib.MeasureTheory.MeasurableSpace.Basic

URI: https://scilib.ai/kg/mathlib#measurable_of_subsingleton_codomain

← MathLib Explorer

English

If β is a subsingleton, any f is measurable.

Русский

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

LaTeX

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

Lean4

@[nontriviality, measurability]
theorem measurable_of_subsingleton_codomain [Subsingleton β] (f : α → β) : Measurable f := fun s _ =>
  Subsingleton.set_cases MeasurableSet.empty MeasurableSet.univ s

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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