rdropWhile_last_not — Mathlib

English

If rdropWhile p l is nonempty, then the last element of it does not satisfy p.

Русский

Если rdropWhile p l непуст, то последний элемент не удовлетворяет p.

LaTeX

$$$\\text{If } (\\mathrm{rdropWhile}\,p(l) \\neq []) \\text{ then } p((\\mathrm{rdropWhile}\,p(l)).\\text{getLast}) \\neq True.$$$

Lean4

theorem rdropWhile_last_not (hl : l.rdropWhile p ≠ []) : ¬p ((rdropWhile p l).getLast hl) :=
  by
  simp_rw [rdropWhile]
  rw [getLast_reverse, head_dropWhile_not p]
  simp

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