mem_of_mem_dropn

Mathlib.Data.WSeq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.mem_of_mem_dropn

English

If some a is in get? s n, then a is in s.

Русский

Если some a ∈ get? s n, то a ∈ s.

LaTeX

$$$$\forall s:\\mathrm{WSeq}\,\alpha,\forall a:\\alpha,\forall n:\\mathbb{N},\ \text{some } a \in \mathrm{get?}\,s\,n \Rightarrow a \in s.$$$$

Lean4

theorem mem_of_mem_dropn {s : WSeq α} {a} : ∀ {n}, a ∈ drop s n → a ∈ s
  | 0, h => h
  | n + 1, h => @mem_of_mem_dropn s a n (mem_of_mem_tail h)

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

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

Разделы

Аффилиация

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