rdrop_eq_reverse_drop_reverse — Mathlib

English

rdrop with respect to a relation R equals reverse(drop reverse) formulation.

Русский

Destutter для отношения R равен обратному применению drop через reverse.

LaTeX

$$$\\mathrm{rdrop}_R(l,n) = \\text{reverse}(\\text{drop}_R(\\text{reverse}(l),n))$$$

Lean4

theorem rdrop_eq_reverse_drop_reverse : l.rdrop n = reverse (l.reverse.drop n) :=
  by
  rw [rdrop]
  induction l using List.reverseRecOn generalizing n with
  | nil => simp
  | append_singleton xs x IH =>
    cases n
    · simp [take_length_add_append]
    · simp [take_append, IH]

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