singleton

Mathlib.Combinatorics.Hindman

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

← MathLib Explorer

English

For any i, the i-th element of the stream lies in FP a: a.get i ∈ FP a.

Русский

Для любого i i-й элемент потока принадлежит FP a: a.get i ∈ FP a.

LaTeX

$$$$ a.get i \in FP\ a $$$$

Lean4

@[to_additive]
theorem singleton {M} [Semigroup M] (a : Stream' M) (i : ℕ) : a.get i ∈ FP a := by
  induction i generalizing a with
  | zero => exact FP.head _
  | succ i ih => exact FP.tail _ _ (ih _)

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

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

Разделы

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

Аффилиация

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