unop_inj_iff

Mathlib.Data.Opposite

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

English

Two elements of αᵒᵖ are equal if their unop images in α are equal.

Русский

Два элемента αᵒᵖ равны тогда и только если их изображения unop в α равны.

LaTeX

$$$\forall x,y:\; unop\ x = unop\ y \iff x = y$$$

Lean4

@[simp]
theorem unop_inj_iff (x y : αᵒᵖ) : unop x = unop y ↔ x = y :=
  unop_injective.eq_iff

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

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

Разделы

Аффилиация

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