equivToOpposite_symm_coe

Mathlib.Data.Opposite

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

English

The inverse of the equivalence corresponds to unop.

Русский

Обратная эквивалентность соответствует unop.

LaTeX

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

Lean4

@[simp]
theorem equivToOpposite_symm_coe : (equivToOpposite.symm : αᵒᵖ → α) = unop :=
  rfl

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

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

Разделы

Аффилиация

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