mono_of_cofibration

Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

URI: https://scilib.ai/kg/mathlib#SSet.modelCategoryQuillen.mono_of_cofibration

English

If a map f of simplicial sets is a monomorphism, then it is a cofibration.

Русский

Если отображение f между симпликальным множеством является монообразом, то оно является кофибрацией.

LaTeX

$$$ [\\text{Mono}(f)] \\Rightarrow \\text{Cofibration}(f)$$$

Lean4

instance mono_of_cofibration [Cofibration f] : Mono f := by rwa [← cofibration_iff]

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

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

Разделы

Аффилиация

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