toRange

Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

URI: https://scilib.ai/kg/mathlib#SSet.Subcomplex.toRange

Lean4

/-- The morphism `X ⟶ Subcomplex.range f` induced by `f : X ⟶ Y`. -/
abbrev toRange : X ⟶ Subcomplex.range f :=
  Subpresheaf.toRange f

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

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

Разделы

Аффилиация

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