instFaithfulForget

Mathlib.Topology.Category.Compactum

URI: https://scilib.ai/kg/mathlib#Compactum.instFaithfulForget

English

The forgetful functor from Compactum is faithful.

Русский

Функтор забывания для Compactum является верным.

LaTeX

$$$\\text{forget.Faithful}$$$

Lean4

instance : forget.Faithful :=
  show (Monad.forget _).Faithful from inferInstance

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

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

Разделы

Аффилиация

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