op_eq_iff_eq_unop

Mathlib.Data.Opposite

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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