drop_append_of_le_length

Mathlib.Data.Stream.Init

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

Lean4

theorem drop_append_of_le_length (h : n ≤ x.length) : (x ++ₛ a).drop n = x.drop n ++ₛ a :=
  by
  obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le h
  ext k; rcases lt_or_ge k m with _ | hk
  · rw [get_drop, get_append_left, get_append_left, List.getElem_drop]; simpa [hm]
  · obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hk
    have hm' : m = (x.drop n).length := by simp [hm]
    simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right]
      -- Take theorem reduces a proof of equality of infinite streams to an
      -- induction over all their finite approximations.

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

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

Разделы

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

Аффилиация

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