rtake_eq_reverse_take_reverse — Mathlib

English

rtake l n equals reverse of taking n elements from the reverse of l.

Русский

rtake l n равен обратному взятию n элементов из обратного списка l.

LaTeX

$$$\\mathrm{rtake}(l,n) = \\mathrm{reverse}(\\mathrm{take}(n,\\ \\mathrm{reverse}(l)))$$$

Lean4

theorem rtake_eq_reverse_take_reverse : l.rtake n = reverse (l.reverse.take n) :=
  by
  rw [rtake]
  induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · exact drop_length
    · simp [drop_append, IH]

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