compl_iff

Mathlib.MeasureTheory.MeasurableSpace.Defs

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

English

MeasurableSet s^c is equivalent to MeasurableSet s.

Русский

Измеримость дополнения s^c эквивалентна измеримости s.

LaTeX

$$$\MeasurableSet(s^c) \iff \MeasurableSet(s)$$$

Lean4

@[simp]
theorem compl_iff : MeasurableSet sᶜ ↔ MeasurableSet s :=
  ⟨.of_compl, .compl⟩

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

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

Разделы

Аффилиация

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