rtakeWhile_concat_neg

Mathlib.Data.List.DropRight

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

English

If p x is false, then rtakeWhile p (l ++ [x]) equals the empty list.

Русский

Если p(x) ложно, то rtakeWhile p (l ++ [x]) = [].

LaTeX

$$$$ \mathrm{rtakeWhile}(p, l ++ [x]) = \emptyset \quad\text{if } p(x) = \text{false}. $$$$

Lean4

@[simp]
theorem rtakeWhile_concat_neg (x : α) (h : ¬p x) : rtakeWhile p (l ++ [x]) = [] := by rw [rtakeWhile_concat, if_neg h]

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

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

Разделы

Аффилиация

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