FP

Mathlib.Combinatorics.Hindman

URI: https://scilib.ai/kg/mathlib#Hindman.FP

Lean4

/-- `FP a` is the set of finite products in `a`, i.e. `m ∈ FP a` if `m` is the product of a nonempty
subsequence of `a`. We give a direct inductive definition instead of talking about subsequences. -/
@[to_additive FS]
inductive FP {M} [Semigroup M] : Stream' M → Set M
  | head' (a : Stream' M) : FP a a.head
  | tail' (a : Stream' M) (m : M) (h : FP a.tail m) : FP a m
  | cons' (a : Stream' M) (m : M) (h : FP a.tail m) : FP a (a.head * m)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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