measurable_fderiv_apply_const

Mathlib.Analysis.Calculus.FDeriv.Measurable

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

← MathLib Explorer

English

The map sending x to fderiv 𝕜 f x is measurable.

Русский

Отображение x ↦ fderiv 𝕜 f x измеримо.

LaTeX

$$$$\text{Measurable}(fderiv 𝕜 f).$$$$

Lean4

@[measurability, fun_prop]
theorem measurable_fderiv_apply_const [MeasurableSpace F] [BorelSpace F] (y : E) : Measurable fun x => fderiv 𝕜 f x y :=
  (ContinuousLinearMap.measurable_apply y).comp (measurable_fderiv 𝕜 f)

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

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

Разделы

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

Аффилиация

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