compl_eq_iff

Mathlib.Order.BooleanAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#IsCompl.compl_eq_iff

English

If h is IsCompl x y, then for all z, zᶜ = y ↔ z = x.

Русский

Если h — IsCompl x y, то для любого z: zᶜ = y ⇔ z = x.

LaTeX

$$If $h$ is IsCompl$(x,y)$, then $z^{c} = y \\Rightarrow z = x$ and conversely.$$

Lean4

theorem compl_eq_iff (h : IsCompl x y) : zᶜ = y ↔ z = x :=
  h.compl_eq ▸ compl_inj_iff

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

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

Разделы

Аффилиация

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