lift_eqToHom_comp

Mathlib.CategoryTheory.FiberedCategory.HomLift

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

English

If h : R' = R, then p.IsHomLift (eqToHom h ≫ f) φ holds whenever p.IsHomLift f φ holds.

Русский

Если h : R' = R, тогда p.IsHomLift (eqToHom h ≫ f) φ сохраняется при наличии p.IsHomLift f φ.

LaTeX

$$$$ p.IsHomLift (eqToHom h \; ≫ \; f) \; \varphi $$$$

Lean4

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

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

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

Разделы

Аффилиация

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