instIsEquivalenceObjPost

Mathlib.CategoryTheory.Comma.Over.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Over.instIsEquivalenceObjPost

English

If G is a right adjoint, then Over.post G is a right adjoint.

Русский

Если G — правый сопряженный, то Over.post G — правый сопряженный.

LaTeX

$$$\\operatorname{IsRightAdjoint}(G) \\Rightarrow \\operatorname{IsRightAdjoint}(\\mathrm{Over.post}\\ G)$$$

Lean4

instance [F.IsEquivalence] : (Over.post (X := X) F).IsEquivalence where

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

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

Разделы

Аффилиация

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