topToDeltaGenerated

Mathlib.Topology.Category.DeltaGenerated

URI: https://scilib.ai/kg/mathlib#DeltaGenerated.topToDeltaGenerated

Lean4

/-- The faithful (but not full) functor taking each topological space to its delta-generated
  coreflection. -/
@[simps!]
def topToDeltaGenerated : TopCat.{u} ⥤ DeltaGenerated.{u}
    where
  obj X := of (DeltaGeneratedSpace.of X)
  map {_ Y}
    f :=
    TopCat.ofHom
      ⟨f, (continuous_to_deltaGenerated (Y := Y)).mpr <| continuous_le_dom deltaGenerated_le f.hom.continuous⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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