instFaithfulTopCatTopCatToCondensedSet

Mathlib.Condensed.TopCatAdjunction

URI: https://scilib.ai/kg/mathlib#CondensedSet.instFaithfulTopCatTopCatToCondensedSet

English

The functor topCatToCondensedSet is faithful.

Русский

Функтор topCatToCondensedSet сохраняет причинность; он верно различает морфизмы.

LaTeX

$$$\mathrm{topCatToCondensedSet}$ is faithful$$

Lean4

instance : topCatToCondensedSet.Faithful :=
  topCatAdjunction.faithful_R_of_epi_counit_app

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

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

Разделы

Аффилиация

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