lift_id_comp

Mathlib.CategoryTheory.FiberedCategory.HomLift

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

English

If hab : a ∼= b and hR : p.obj a = R, then p.IsHomLift (eqToHom hRS) (eqToHom hab).

Русский

Если a эквивалентно b и p.obj a = R, тогда p.IsHomLift (eqToHom hRS) (eqToHom hab).

LaTeX

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

Lean4

instance lift_id_comp : p.IsHomLift (𝟙 R ≫ f) φ := by simp_all

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

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

Разделы

Аффилиация

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