instIsEquivalenceMapOfIsIso

Mathlib.CategoryTheory.Comma.Over.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Under.instIsEquivalenceMapOfIsIso

English

If f is an isomorphism, then Under.map f is an equivalence.

Русский

Если f — изоморфизм, то Under.map f является эквивалентностью.

LaTeX

$$If $f$ is an isomorphism, then $(\\mathrm{Under.map} f)$ is an equivalence.$$

Lean4

instance [IsIso f] : (Under.map f).IsEquivalence :=
  (Under.mapIso <| asIso f).isEquivalence_functor

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

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

Разделы

Аффилиация

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