rdropWhile_append_rtakeWhile — Mathlib

English

The concatenation of rdropWhile p l with rtakeWhile p l equals l.

Русский

Соединение rdropWhile p l и rtakeWhile p l образует исходный список l.

LaTeX

$$$$ \mathrm{rdropWhile}(p, l) \;\mathbin{+}\; \mathrm{rtakeWhile}(p, l) = l. $$$$

Lean4

@[simp]
theorem rdropWhile_append_rtakeWhile : l.rdropWhile p ++ l.rtakeWhile p = l :=
  by
  simp only [rdropWhile, rtakeWhile]
  rw [← List.reverse_append, takeWhile_append_dropWhile, reverse_reverse]

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