rtake_concat_succ

Mathlib.Data.List.DropRight

URI: https://scilib.ai/kg/mathlib#List.rtake_concat_succ

English

simplicity: rtake (l ++ [x]) (n+1) = rtake l n ++ [x].

Русский

rtake (l ++ [x]) (n+1) = rtake l n ++ [x].

LaTeX

$$$\\mathrm{rtake}(l \\cup \\{x\\}, n+1) = \\mathrm{rtake}(l, n) \\cup \\{x\\}$$$

Lean4

@[simp]
theorem rtake_concat_succ (x : α) : rtake (l ++ [x]) (n + 1) = rtake l n ++ [x] := by
  simp [rtake_eq_reverse_take_reverse]

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

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

Разделы

Аффилиация

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