rdropWhile_concat — Mathlib

English

rdropWhile p on a concatenation l ++ [x] equals: if p x then rdropWhile p l else l ++ [x].

Русский

rdropWhile p на конкатенации l ++ [x] равен: если p x, то rdropWhile p l, иначе l ++ [x].

LaTeX

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

Lean4

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

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