compl_inj_iff

Mathlib.Order.BooleanAlgebra.Basic

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

English

xᶜ = yᶜ ↔ x = y.

Русский

xᶜ = yᶜ ⇔ x = y.

LaTeX

$$$x^{c} = y^{c} \\iff x = y$$$

Lean4

@[simp]
theorem compl_inj_iff : xᶜ = yᶜ ↔ x = y :=
  compl_injective.eq_iff

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

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

Разделы

Аффилиация

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