rdropWhile_eq_nil_iff — Mathlib

English

For any p and list l, the value of rdropWhile p l is the empty list iff p holds for every element of l.

Русский

Для любого p и списка l значение rdropWhile p l равно пустому списку тогда и только тогда, когда p истинно для каждого элемента l.

LaTeX

$$$$ \mathrm{rdropWhile}(p, l) = \varnothing \quad\Longleftrightarrow\quad \forall x \in l,\ p(x) = \text{true}. $$$$

Lean4

@[simp]
theorem rdropWhile_eq_nil_iff : rdropWhile p l = [] ↔ ∀ x ∈ l, p x := by simp [rdropWhile]

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