of_subsingleton_dom

Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEStronglyMeasurable.of_subsingleton_dom

← MathLib Explorer

English

If the domain is a subsingleton, any function is AEStronglyMeasurable.

Русский

Если область домена несвязна (односвязна), любая функция AEStronglyMeasurable.

LaTeX

$$$ [Subsingleton\\ α] : \\text{AEStronglyMeasurable}\\ f\\ μ $$$

Lean4

@[simp, nontriviality]
theorem of_subsingleton_dom [Subsingleton α] : AEStronglyMeasurable[m] f μ :=
  StronglyMeasurable.of_subsingleton_dom.aestronglyMeasurable

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

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

Разделы

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

Аффилиация

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