isEquivalence_preRight

Mathlib.CategoryTheory.Comma.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Comma.isEquivalence_preRight

← MathLib Explorer

English

If F is an equivalence, then post L R F is an equivalence.

Русский

Если F — эквивалентность, то post L R F — эквивалентность.

LaTeX

$$$F\text{ IsEquivalence} \Rightarrow (\text{post } L R F)\text{ IsEquivalence}$$$

Lean4

/-- If `F` is an equivalence, then so is `preRight L F R`. -/
instance isEquivalence_preRight (L : A ⥤ T) (F : C ⥤ B) (R : B ⥤ T) [F.IsEquivalence] : (preRight L F R).IsEquivalence
    where

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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