forgetToTop_faithful

Mathlib.Topology.Order.Category.AlexDisc

URI: https://scilib.ai/kg/mathlib#AlexDisc.forgetToTop_faithful

English

The forgetful functor from Alexandrov-discrete spaces to topological spaces is faithful.

Русский

Забывающий функтор от пространств Александрово-дискретных к топологическим пространствам верен.

LaTeX

$$$\mathrm{Faithful}(\mathrm{forget}_{AlexDisc\to TopCat})$$$

Lean4

instance forgetToTop_faithful : (forget₂ AlexDisc TopCat).Faithful where

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

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

Разделы

Аффилиация

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