sup_of_right

Mathlib.MeasureTheory.MeasurableSpace.Basic

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

← MathLib Explorer

English

If the codomain is a subsingleton, any f is measurable.

Русский

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

LaTeX

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

Lean4

theorem sup_of_right {mα mα' : MeasurableSpace α} {_ : MeasurableSpace β} {f : α → β} (h : Measurable[mα'] f) :
    Measurable[mα ⊔ mα'] f :=
  h.mono le_sup_right le_rfl

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

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

Разделы

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

Аффилиация

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