measurable

Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.measurable

English

A continuous linear map between normed spaces is a measurable function.

Русский

Непрерывно-линейное отображение между нормированными пространствами измеримо.

LaTeX

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

Lean4

@[fun_prop, measurability]
protected theorem measurable (L : E →L[R] F) : Measurable L :=
  L.continuous.measurable

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

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

Разделы

Аффилиация

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