equivToOpposite_coe

Mathlib.Data.Opposite

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

English

The equivalence equivToOpposite acts as the op function on objects.

Русский

Эквивалентность equivToOpposite действует как операнд op на объектах.

LaTeX

$$$(equivToOpposite : α \to α^\mathrm{op}) = \mathrm{op}$$$

Lean4

@[simp]
theorem equivToOpposite_coe : (equivToOpposite : α → αᵒᵖ) = op :=
  rfl

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

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

Разделы

Аффилиация

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