instFibrationPTrivialCofibrationsFibrations

Mathlib.AlgebraicTopology.ModelCategory.Instances

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations

English

Given a data h of the form MapFactorizationData with trivial cofibrations and fibrations, the associated p is a fibration.

Русский

Дано разложение морфизма через тривиальные кофибрации и фибрации; соответствующий отображение является фибрацией.

LaTeX

$$Fibration h.p$$

Lean4

instance : Fibration h.p := by simpa only [fibration_iff] using h.hp

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

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

Разделы

Аффилиация

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