I_le_monomorphisms

Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

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

English

The class I is contained in the class of monomorphisms; every element of I is a mono morphism.

Русский

Класс I содержится в классе мономорфизмов; каждый элемент I является монообразом.

LaTeX

$$$ I \\subseteq \\mathrm{Monomorphisms}$$$

Lean4

theorem I_le_monomorphisms : I.{u} ≤ monomorphisms _ :=
  by
  rintro _ _ _ ⟨n⟩
  exact monomorphisms.infer_property _

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

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

Разделы

Аффилиация

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