equivalence₁CounitIso_eq

Mathlib.AlgebraicTopology.DoldKan.Compatibility

URI: https://scilib.ai/kg/mathlib#AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_eq

English

An alternate version of the Limit Iso Pi Hom-Comp Pi relation holds.

Русский

Существует ещё одна версия равенства hom-проекции в отношении Limit Iso Pi.

LaTeX

$$$\\text{AltHomCompPi}$$$

Lean4

theorem equivalence₁CounitIso_eq : (equivalence₁ hF).counitIso = equivalence₁CounitIso hF :=
  by
  ext Y
  simp [equivalence₁, equivalence₀]

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

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

Разделы

Аффилиация

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