instFiniteSym

Mathlib.Data.Finite.Vector

URI: https://scilib.ai/kg/mathlib#instFiniteSym

English

If α is a finite type, then for every natural number n, the type Sym α n is finite.

Русский

Пусть α — конечный тип; тогда для любого натурального числа n тип Sym α n конечен.

LaTeX

$$$$ \forall {\alpha : Type u} [Finite \alpha] {n : \Nat}, Finite (Sym \alpha n) $$$$

Lean4

instance [Finite α] {n : ℕ} : Finite (Sym α n) := by
  classical
  haveI := Fintype.ofFinite α
  infer_instance

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

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

Разделы

Аффилиация

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