measurableSet_Ioo

Mathlib.Analysis.BoxIntegral.Partition.Measure

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Box.measurableSet_Ioo

English

The open-interval box Box.Ioo(I) is measurable.

Русский

Открытое поР коробки Box.Ioo(I) измеримо.

LaTeX

$$$\\text{MeasurableSet}(Box.Ioo(I))$$$

Lean4

theorem measurableSet_Ioo : MeasurableSet (Box.Ioo I) :=
  MeasurableSet.univ_pi fun _ => _root_.measurableSet_Ioo

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

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

Разделы

Аффилиация

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