sound

Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.RightHomotopyClass.sound

English

If two maps are related by a right homotopy, then their corresponding mk values are equal.

Русский

Если f и g гомотопны справа, то их значения mk равны.

LaTeX

$$$mk\, f = mk\, g$$$

Lean4

theorem sound [CategoryWithWeakEquivalences C] {f g : X ⟶ Y} (h : RightHomotopyRel f g) : mk f = mk g :=
  Quot.sound h

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

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

Разделы

Аффилиация

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