isEquivalence_functor

Mathlib.CategoryTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.isEquivalence_functor

English

The inverse equivalence has essentially surjective functor, mirroring essSurj_functor for the forward direction.

Русский

Обратная эквивалентность имеет существенную сюръектность функторов, аналогично essSurj_functor для прямого направления.

LaTeX

$$$e.inverse.EssSurj$$$

Lean4

instance isEquivalence_functor (F : C ≌ D) : IsEquivalence F.functor where

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

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

Разделы

Аффилиация

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