rdropWhile_reverse — Mathlib

English

If we reverse the list, rdropWhile corresponds to dropWhile on the reversed list: l.reverse.rdropWhile p = (l.dropWhile p).reverse.

Русский

Если развернуть список, rdropWhile эквивалентно dropWhile на развернутом списке: l.reverse.rdropWhile p = (l.dropWhile p).reverse.

LaTeX

$$$$ \mathrm{rdropWhile}(p, \mathrm{reverse}(l)) = \mathrm{reverse}(\mathrm{takeWhile}(p, l)). $$$$

Lean4

theorem rdropWhile_reverse : l.reverse.rdropWhile p = (l.dropWhile p).reverse := by
  simp_rw [rdropWhile, reverse_reverse]

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