measurableSet_Icc

Mathlib.Analysis.BoxIntegral.Partition.Measure

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

English

The closed-box interior, Box.Icc(I), is a measurable set.

Русский

Замкнутое ограничение Box.Icc(I) является измеримым множеством.

LaTeX

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

Lean4

theorem measurableSet_Icc : MeasurableSet (Box.Icc I) :=
  _root_.measurableSet_Icc

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

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

Разделы

Аффилиация

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