instFullLightCondensedTypeDiscrete

Mathlib.Condensed.Discrete.LocallyConstant

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

English

The discrete LightCondensed type is full.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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