lift_comp_eqToHom

Mathlib.CategoryTheory.FiberedCategory.HomLift

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

English

If hab : a = b and hS : p.obj b = S, then p.IsHomLift (eqToHom hRS) (eqToHom hab) holds.

Русский

Если a = b и p.obj b = S, тогда p.IsHomLift (eqToHom hRS) (eqToHom hab).

LaTeX

$$$$ p.IsHomLift (eqToHom hRS) (eqToHom hab) $$$$

Lean4

instance lift_comp_eqToHom {S' : 𝒮} (h : S = S') : p.IsHomLift (f ≫ eqToHom h) φ := by subst h; simp_all

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

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

Разделы

Аффилиация

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