compl_involutive

Mathlib.Order.BooleanAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#compl_involutive

English

compl is an involution: for all x, compl(compl x) = x.

Русский

комплемент является инволюцией: для всех x, compl(compl x) = x.

LaTeX

$$$\\forall x, \\; x^{c\\,c} = x$$$

Lean4

@[simp]
theorem compl_involutive : Function.Involutive (compl : α → α) :=
  compl_compl

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

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

Разделы

Аффилиация

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