instFintype

Mathlib.Data.Fintype.Sigma

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

English

The dependent sigma-type Σ' i, κ i is finite; there is an explicit finite enumeration via an equivalence.

Русский

Зависимый PSigma-тип Σ' i, κ i конечен; существует явное конечное перечисление через эквивалентность.

LaTeX

$$$\text{Fintype}(\Sigma' i, κ i)$$$

Lean4

instance instFintype : Fintype (Σ' i, κ i) :=
  .ofEquiv _ (Equiv.psigmaEquivSigma _).symm

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

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

Разделы

Аффилиация

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