instIsEquivalenceOppositeLeftOp

Mathlib.CategoryTheory.Opposites

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instIsEquivalenceOppositeLeftOp

English

If F is an equivalence, then F.leftOp is an equivalence.

Русский

Если F является эквивалентностью, то F.leftOp — эквивалентность.

LaTeX

$$$\text{If } F:\, C \to D^{op} \text{ is IsEquivalence, then } F.leftOp:\, C^{op} \to D \text{ is IsEquivalence}$$$

Lean4

instance {F : C ⥤ Dᵒᵖ} [IsEquivalence F] : IsEquivalence F.leftOp where

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

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

Разделы

Аффилиация

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