isEquivalence_left_of_isEquivalence_right

Mathlib.CategoryTheory.Adjunction.FullyFaithful

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Adjunction.isEquivalence_left_of_isEquivalence_right

English

If h: L ⊣ R and R is an equivalence, L is an equivalence.

Русский

Пусть h: L ⊣ R и R эквивалентен; тогда L эквивалентен.

LaTeX

$$$\text{isEquivalence_left_of_isEquivalence_right}(h) : (R.IsEquivalence) \Rightarrow (L.IsEquivalence)$$$

Lean4

theorem isEquivalence_left_of_isEquivalence_right (h : L ⊣ R) [R.IsEquivalence] : L.IsEquivalence :=
  h.toEquivalence.isEquivalence_functor

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

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

Разделы

Аффилиация

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