rdropWhile_singleton — Mathlib

English

For a singleton list [x], rdropWhile p [x] equals [] if p x is true, otherwise [x].

Русский

Для списка-одиночки [x], rdropWhile p [x] равен [] если p x истинно, иначе [x].

LaTeX

$$$\\mathrm{rdropWhile}\,p([x]) = \\begin{cases} [] & p(x) = True \\\\ [x] & p(x) = False \\end{cases}$$$

Lean4

theorem rdropWhile_singleton (x : α) : rdropWhile p [x] = if p x then [] else [x] := by
  rw [← nil_append [x], rdropWhile_concat, rdropWhile_nil]

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