rtakeWhile_eq_nil_iff — Mathlib

English

rtakeWhile p l = empty iff for every nonempty l, last(l) does not satisfy p.

Русский

rtakeWhile p l = [] тогда и только тогда, когда для каждого непустого l последнее l не удовлетворяет p.

LaTeX

$$$$ \mathrm{rtakeWhile}(p, l) = \emptyset \iff \forall hl\,(l \neq \varnothing \Rightarrow p(\mathrm{last}(l)) = \text{false}). $$$$

Lean4

@[simp]
theorem rtakeWhile_eq_nil_iff : rtakeWhile p l = [] ↔ ∀ hl : l ≠ [], ¬p (l.getLast hl) := by
  induction l using List.reverseRecOn <;> simp [rtakeWhile]

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