instFaithfulLightCondensedTypeDiscrete

Mathlib.Condensed.Discrete.LocallyConstant

URI: https://scilib.ai/kg/mathlib#LightCondSet.LocallyConstant.instFaithfulLightCondensedTypeDiscrete

English

The discrete LightCondensed type functor is faithful.

Русский

Дискретный функтор LightCondensed типа верен.

LaTeX

$$$\operatorname{Faithful}\bigl(\mathrm{LightCondensed.discrete}(\mathrm{Type}\,u)\bigr)$$$

Lean4

instance : (LightCondensed.discrete (Type u)).Faithful :=
  Functor.Faithful.of_iso iso.{u}

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

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

Разделы

Аффилиация

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