FS

Mathlib.Combinatorics.Hindman

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

Lean4

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

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

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

Разделы

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

Аффилиация

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