measurableSet_interior

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

URI: https://scilib.ai/kg/mathlib#measurableSet_interior

English

The interior of any set is measurable.

Русский

Внутренность любого множества измерима.

LaTeX

$$$$ \text{MeasurableSet}(\operatorname{interior}(s)). $$$$

Lean4

@[measurability]
theorem measurableSet_interior : MeasurableSet (interior s) :=
  isOpen_interior.measurableSet

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

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

Разделы

Аффилиация

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