measurableSet

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

URI: https://scilib.ai/kg/mathlib#IsCompact.measurableSet

English

A compact set in a T2 space is measurable.

Русский

Компактное множество в металлоподобном пространстве измеримо.

LaTeX

$$$$ \text{MeasurableSet}(s) \quad \text{if } s \text{ is compact and } [T2Space]. $$$$

Lean4

theorem measurableSet [T2Space α] (h : IsCompact s) : MeasurableSet s :=
  h.isClosed.measurableSet

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

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

Разделы

Аффилиация

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