op_injective — Mathlib

English

If two object properties have the same opposite, then they are equal. In other words, the op operation on object properties is injective.

Русский

Если два свойства объектов имеют одинаковый противоположный объект, то они равны. То есть операция оппонента над свойствами объектов инъективна.

LaTeX

$$$P^{op} = Q^{op} \Rightarrow P = Q$$$

Lean4

theorem op_injective {P Q : ObjectProperty C} (h : P.op = Q.op) : P = Q := by rw [← P.unop_op, ← Q.unop_op, h]

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