measurable_compl

Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

English

The map taking a set to its complement is measurable.

Русский

Отображение, отправляющее множество в его дополнение, измеримо.

LaTeX

$$$\mathrm{Measurable}\bigl((\cdot)^c\bigr) : \mathrm{Set}(\alpha) \to \mathrm{Set}(\alpha)$$$

Lean4

theorem measurable_compl : Measurable ((·ᶜ) : Set α → Set α) :=
  measurable_set_iff.2 fun _ ↦ measurable_set_notMem _

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

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

Разделы

Аффилиация

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