isEquivalence_right_of_isEquivalence_left

Mathlib.CategoryTheory.Adjunction.FullyFaithful

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

English

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

Русский

Если h: L ⊣ R и L эквивалентен, то R эквивалентен.

LaTeX

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

Lean4

theorem isEquivalence_right_of_isEquivalence_left (h : L ⊣ R) [L.IsEquivalence] : R.IsEquivalence :=
  h.toEquivalence.isEquivalence_inverse

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

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

Разделы

Аффилиация

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