rtakeWhile_concat — Mathlib

English

For any x, rtakeWhile p of l concatenated with [x] equals if p(x) then rtakeWhile p l concatenated with [x] else [].

Русский

Для любого элемента x: rtakeWhile p (l ++ [x]) равно, если p(x) истинно, то rtakeWhile p l ++ [x], иначе [].

LaTeX

$$$$ \mathrm{rtakeWhile}(p, l ++ [x]) = \begin{cases} \mathrm{rtakeWhile}(p, l) ++ [x], & p(x) = \text{true}, \\ [], & p(x) = \text{false}. \end{cases} $$$$

Lean4

theorem rtakeWhile_concat (x : α) : rtakeWhile p (l ++ [x]) = if p x then rtakeWhile p l ++ [x] else [] :=
  by
  simp only [rtakeWhile, takeWhile, reverse_append, reverse_singleton, singleton_append]
  split_ifs with h <;> simp [h]

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