compl_setOf

Mathlib.Order.BooleanAlgebra.Set

URI: https://scilib.ai/kg/mathlib#Set.compl_setOf

English

The complement of the set {a | p(a)} equals {a | ¬p(a)}.

Русский

Комплемент множества {a | p(a)} равен {a | ¬p(a)}.

LaTeX

$$$\{a\mid p(a)\}^{c} = \{a\mid \neg p(a)\}$.$$

Lean4

theorem compl_setOf {α} (p : α → Prop) : {a | p a}ᶜ = {a | ¬p a} :=
  rfl

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

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

Разделы

Аффилиация

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