eqToHom_comp_lift

Mathlib.CategoryTheory.FiberedCategory.HomLift

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsHomLift.eqToHom_comp_lift

English

If φ lifts f, then φ ≫ eqToHom h lifts f ≫ eqToHom h.

Русский

Если φ поднимает f, то φ ≫ eqToHom h поднимает f ≫ eqToHom h.

LaTeX

$$$$ p.IsHomLift f (\varphi \gg eqToHom h) \Rightarrow p.IsHomLift f (\varphi) $$$$

Lean4

instance eqToHom_comp_lift {b' : 𝒳} (h : b = b') : p.IsHomLift f (φ ≫ eqToHom h) := by subst h; simp_all

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

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

Разделы

Аффилиация

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