instCofibrationITrivialCofibrationsFibrations

Mathlib.AlgebraicTopology.ModelCategory.Instances

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

English

If MapFactorizationData is given from trivialCofibrations to fibrations, then h.i is a Cofibration.

Русский

Если имеется факторизационная data через тривиальные кофибрации к фибрациям, то h.i является кофибрацией.

LaTeX

$$$\text{Cofibration } h.i$$$

Lean4

instance : Cofibration h.i := by simpa only [cofibration_iff] using h.hi.1

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

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

Разделы

Аффилиация

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