op_inj_iff

Mathlib.Data.Opposite

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

English

Two opposite elements are equal after applying op if and only if the original elements are equal.

Русский

Два элемента в противоположном типе равны после применения op тогда и только если исходные элементы равны.

LaTeX

$$$\forall x,y:\ α,\; op\ x = op\ y \iff x = y$$$

Lean4

theorem op_inj_iff (x y : α) : op x = op y ↔ x = y :=
  op_injective.eq_iff

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

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

Разделы

Аффилиация

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