instFintypeSubtypeEqNatSemilength

Mathlib.Combinatorics.Enumerative.DyckWord

URI: https://scilib.ai/kg/mathlib#DyckWord.instFintypeSubtypeEqNatSemilength

English

There is a finite type structure on the subtype { p ∈ DyckWord | p.semilength = n } for each n.

Русский

Для каждого n существует конечная структура типа подмножества { p ∈ DyckWord | p.semilength = n }.

LaTeX

$${n : ℕ} → Fintype { p : DyckWord // Eq p.semilength n }$$

Lean4

instance {n : ℕ} : Fintype { p : DyckWord // p.semilength = n } :=
  Fintype.ofEquiv _ (equivTreesOfNumNodesEq n).symm

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

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

Разделы

Аффилиация

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