rtakeWhile_reverse — Mathlib

English

Taking while from the reverse is the reverse of taking while from the original list.

Русский

Взятие префикса с условием в обратном порядке равно обратному взятию префикса из исходного списка.

LaTeX

$$$\forall \alpha\; p:\alpha \to Bool\; l:\ List\;\alpha,\; l.\operatorname{rtakeWhile} p = (l.\operatorname{takeWhile} p).\operatorname{reverse}$$$

Lean4

theorem rtakeWhile_reverse : l.reverse.rtakeWhile p = (l.takeWhile p).reverse := by
  simp_rw [rtakeWhile, reverse_reverse]

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