unop_eq_iff_eq_op

Mathlib.Data.Opposite

URI: https://scilib.ai/kg/mathlib#Opposite.unop_eq_iff_eq_op

English

An equality of an unop-applied element with another is equivalent to equality of the original element with op of that element.

Русский

Равенство unop x = y эквивалентно равенству x = op y.

LaTeX

$$$\forall x:\; α^\mathrm{op},\; \forall y:\; α,\; unop\ x = y \iff x = op\ y$$$

Lean4

theorem unop_eq_iff_eq_op {x} {y : α} : unop x = y ↔ x = op y :=
  equivToOpposite.symm.apply_eq_iff_eq_symm_apply

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

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

Разделы

Аффилиация

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