of_compl

Mathlib.Topology.Baire.BaireMeasurable

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

English

If sᶜ is BaireMeasurableSet, then s is BaireMeasurableSet.

Русский

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

LaTeX

$$$$ \mathrm{BaireMeasurableSet}(s^{c}) \Rightarrow \mathrm{BaireMeasurableSet}(s). $$$$

Lean4

theorem of_compl (h : BaireMeasurableSet sᶜ) : BaireMeasurableSet s :=
  MeasurableSet.of_compl h

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

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

Разделы

Аффилиация

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