not

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#Measurable.not

English

If p is measurable, then the negation ¬p is also measurable.

Русский

Если p измерим, то и отрицание ¬p тоже измеримо.

LaTeX

$$$\mathrm{Measurable}(p) \Rightarrow \mathrm{Measurable}(\lambda x. \neg p(x))$$$

Lean4

theorem not (hp : Measurable p) : Measurable (¬p ·) :=
  measurableSet_setOf.1 hp.setOf.compl

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

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

Разделы

Аффилиация

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