op_inj

Mathlib.Algebra.Opposites

URI: https://scilib.ai/kg/mathlib#MulOpposite.op_inj

English

For all x, y, op(x) = op(y) if and only if x = y.

Русский

Для всех x, y верно: op(x) = op(y) тогда и только если x = y.

LaTeX

$$$\\\\mathrm{op}(x)=\\\\mathrm{op}(y) \\\\iff x=y$$$

Lean4

@[to_additive (attr := simp)]
theorem op_inj {x y : α} : op x = op y ↔ x = y :=
  iff_of_eq <| PreOpposite.op'.injEq _ _

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

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

Разделы

Аффилиация

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