measurableSpace

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

URI: https://scilib.ai/kg/mathlib#EReal.measurableSpace

English

The space of continuous linear maps E →L[𝕜] F is equipped with a borel measurable space.

Русский

Пространство непрерывных линейных отображений E →L[𝕜] F наделено борелевым сигма-алгеброй измеримости.

LaTeX

$$MeasurableSpace (E →L[𝕜] F) = borel _$$

Lean4

instance measurableSpace : MeasurableSpace EReal :=
  borel EReal

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

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

Разделы

Аффилиация

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