compl_singleton

Mathlib.Data.Bool.Set

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

English

The complement of {b} is the singleton {not b}.

Русский

Дополнение множества {b} равно односоставному множеству {¬b}.

LaTeX

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

Lean4

@[simp, grind =]
theorem compl_singleton (b : Bool) : ({ b }ᶜ : Set Bool) = {!b} := by grind [cases Bool]

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

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

Разделы

Аффилиация

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