instFintype

Mathlib.Data.Fintype.Shrink

URI: https://scilib.ai/kg/mathlib#Shrink.instFintype

English

Shrink α is finite when α is finite; in fact Shrink α is in bijection with α.

Русский

Shrink α конечен, если α конечен; фактически Shrink α эквивалентно α.

LaTeX

$$$\Shrink(\alpha) \cong α$$$

Lean4

noncomputable instance instFintype : Fintype (Shrink.{v} α) :=
  .ofEquiv _ (equivShrink _)

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

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

Разделы

Аффилиация

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