of_subsingleton_dom

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

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

← MathLib Explorer

English

If the domain is a singleton, any function is strongly measurable.

Русский

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

LaTeX

$$[Subsingleton α] ⇒ StronglyMeasurable f$$

Lean4

@[simp, nontriviality]
theorem of_subsingleton_dom [Subsingleton α] : StronglyMeasurable f :=
  ⟨fun _ => SimpleFunc.ofFinite f, fun _ => tendsto_const_nhds⟩

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

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

Разделы

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

Аффилиация

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