take_theorem

Mathlib.Data.Stream.Init

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

Lean4

theorem take_theorem (s₁ s₂ : Stream' α) (h : ∀ n : ℕ, take n s₁ = take n s₂) : s₁ = s₂ :=
  by
  ext n
  induction n with
  | zero => simpa [take] using h 1
  | succ
    n =>
    have h₁ : some (get s₁ (succ n)) = some (get s₂ (succ n)) := by
      rw [← getElem?_take_succ, ← getElem?_take_succ, h (succ (succ n))]
    injection h₁

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

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

Разделы

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

Аффилиация

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