rdropWhile_prefix — Mathlib

English

Let p be a predicate p: α → Bool and l a list. Then the list obtained by removing from the end of l while p holds at the end is a prefix of l; i.e., the result l rdropWhile p is a prefix of l.

Русский

Пусть p: α → Bool и список l. Тогда список, полученный удалением с конца l, пока p возвращает истину, является префиксом l; т.е. l.rdropWhile p является префиксом l.

LaTeX

$$$$ \text{rdropWhile}(p, l) \text{ is a prefix of } l. $$$$

Lean4

theorem rdropWhile_prefix : l.rdropWhile p <+: l :=
  by
  rw [← reverse_suffix, rdropWhile, reverse_reverse]
  exact dropWhile_suffix _

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