measurable_apply'

Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.measurable_apply'

← MathLib Explorer

English

The real numbers are a Borel space (again).

Русский

Числа Реальные — пространство Бореля (повтор).

LaTeX

$$BorelSpace\\, \\mathbb{R}$$

Lean4

@[measurability]
theorem measurable_apply' [MeasurableSpace E] [OpensMeasurableSpace E] [MeasurableSpace F] [BorelSpace F] :
    Measurable fun (x : E) (f : E →L[𝕜] F) => f x :=
  measurable_pi_lambda _ fun f => f.measurable

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

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

Разделы

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

Аффилиация

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