compl_bijective

Mathlib.Order.BooleanAlgebra.Basic

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

English

compl is bijective.

Русский

комплемент — биекция.

LaTeX

$$$\\text{compl} : \\alpha \\to \\alpha \\text{ is bijective}$$$

Lean4

theorem compl_bijective : Function.Bijective (compl : α → α) :=
  compl_involutive.bijective

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

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

Разделы

Аффилиация

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