instFullFunctor

Mathlib.Condensed.Discrete.LocallyConstant

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

English

The discrete LightCondensed type is full.

Русский

Дискретный тип LightCondensed полно.

LaTeX

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

Lean4

instance : LightCondSet.LocallyConstant.functor.Full :=
  functorFullyFaithful.full

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

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

Разделы

Аффилиация

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