compl_singleton

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#Prop.compl_singleton

English

For any p, the complement of the singleton {p} in sets of propositions equals the singleton {¬p}.

Русский

Для любого p дополнение множества {p} в множествах пропозиций равно единственному элементу {¬p}.

LaTeX

$$$\\{p\\}^c = \\{\\\\neg p\\\\}$$$

Lean4

@[simp]
theorem compl_singleton (p : Prop) : ({ p }ᶜ : Set Prop) = {¬p} :=
  ext fun q ↦ by simpa [@Iff.comm q] using not_iff

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

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

Разделы

Аффилиация

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