take_take

Mathlib.Data.Stream.Init

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

Lean4

@[simp]
theorem take_take {s : Stream' α} : ∀ {m n}, (s.take n).take m = s.take (min n m)
  | 0, n => by rw [Nat.min_zero, List.take_zero, take_zero]
  | m, 0 => by rw [Nat.zero_min, take_zero, List.take_nil]
  | m + 1, n + 1 => by rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take]

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

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

Разделы

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

Аффилиация

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