rdropWhile_eq_self_iff — Mathlib

English

The equality rdropWhile p l = l holds exactly when the last element of l does not satisfy p (in particular, for any nonempty l).

Русский

Равенство rdropWhile p l = l выполняется тогда и только тогда, когда последний элемент l не удовлетворяет p (в частности, для любого непустого l).

LaTeX

$$$$ \mathrm{rdropWhile}(p, l) = l \quad\Longleftrightarrow\quad \forall hl\, (l \neq \varnothing)\ \Rightarrow\ p(\text{last}(l)) = \text{false}. $$$$

Lean4

@[simp]
theorem rdropWhile_eq_self_iff : rdropWhile p l = l ↔ ∀ hl : l ≠ [], ¬p (l.getLast hl) := by
  simp [rdropWhile, reverse_eq_iff, getLast_eq_getElem, Nat.pos_iff_ne_zero]

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