instQuasiIsoInv

Mathlib.Algebra.Homology.QuasiIso

URI: https://scilib.ai/kg/mathlib#instQuasiIsoInv

English

If e is a homotopy equivalence, then its inverse e.inv is a quasi-isomorphism.

Русский

Если e — гомотопная эквивалентность, то её обратное e.inv — квазиизоморфизм.

LaTeX

$$$\text{QuasiIso}(e^{-1})$$$

Lean4

instance : QuasiIso e.inv :=
  (inferInstance : QuasiIso e.symm.hom)

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

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

Разделы

Аффилиация

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