instFaithfulTopCatTopToDeltaGenerated

Mathlib.Topology.Category.DeltaGenerated

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

English

The functor deltaGeneratedToTop is faithful.

Русский

Функтор deltaGeneratedToTop верен.

LaTeX

$$$\\forall A,B \\; f,g: A \\to B,\\ (\\deltaGeneratedToTop)(f) = (\\deltaGeneratedToTop)(g) \\Rightarrow f = g.$$$

Lean4

instance : topToDeltaGenerated.{u}.Faithful :=
  ⟨fun h ↦ by ext x; exact CategoryTheory.congr_fun h x⟩

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

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

Разделы

Аффилиация

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