of_compl

Mathlib.MeasureTheory.MeasurableSpace.Defs

URI: https://scilib.ai/kg/mathlib#MeasurableSet.of_compl

English

If the complement of a set s is measurable, then s is measurable as well.

Русский

Если множество дополнения к s измеримо, то само множество s также измеримо.

LaTeX

$$$$ \\text{MeasurableSet}(s^{c}) \\Rightarrow \\text{MeasurableSet}(s). $$$$

Lean4

protected theorem of_compl (h : MeasurableSet sᶜ) : MeasurableSet s :=
  compl_compl s ▸ h.compl

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

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

Разделы

Аффилиация

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