instFullTopCatDeltaGeneratedToTop

Mathlib.Topology.Category.DeltaGenerated

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

← MathLib Explorer

English

The functor deltaGeneratedToTop is full.

Русский

Функтор deltaGeneratedToTop полон.

LaTeX

$$$\\forall A,B \\in \\mathrm{Obj}(\\DeltaGenerated),\\; \\mathrm{Hom}_{\\DeltaGenerated}(A,B) \\to \\mathrm{Hom}_{\\mathrm{TopCat}}((\\deltaGeneratedToTop)(A),(\\deltaGeneratedToTop)(B))$ is surjective.$$

Lean4

instance : deltaGeneratedToTop.{u}.Full :=
  fullyFaithfulDeltaGeneratedToTop.full

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

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

Разделы

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

Аффилиация

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