measurableSet_frontier

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

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

English

The boundary (frontier) of any set is a measurable set.

Русский

Граница любого множества является измеримым множеством.

LaTeX

$$$\\operatorname{MeasurableSet}(\\operatorname{frontier}(s)).$$$

Lean4

@[measurability]
theorem measurableSet_frontier : MeasurableSet (frontier s) :=
  measurableSet_closure.diff measurableSet_interior

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

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

Разделы

Аффилиация

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