rtakeWhile_eq_self_iff

Mathlib.Data.List.DropRight

URI: https://scilib.ai/kg/mathlib#List.rtakeWhile_eq_self_iff

English

rtakeWhile p l = l if and only if p holds for all elements of l.

Русский

rtakeWhile p l = l тогда и только тогда, когда p истинно для каждого элемента l.

LaTeX

$$$$ \mathrm{rtakeWhile}(p, l) = l \iff \forall x \in l,\ p(x) = \text{true}. $$$$

Lean4

@[simp]
theorem rtakeWhile_eq_self_iff : rtakeWhile p l = l ↔ ∀ x ∈ l, p x := by simp [rtakeWhile, reverse_eq_iff]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru