measurableSpace

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

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

English

The real numbers are equipped with the measurable space of Borel sets.

Русский

Действительные числа оснащены измеримым пространством борелевых множеств.

LaTeX

$$MeasurableSpace\\, \\mathbb{R} = borel\\, \\mathbb{R}$$

Lean4

instance measurableSpace : MeasurableSpace ℝ :=
  borel ℝ

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

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

Разделы

Аффилиация

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