rdropWhile_concat_pos

Mathlib.Data.List.DropRight

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

English

If p x holds, then rdropWhile p (l ++ [x]) equals rdropWhile p l.

Русский

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

LaTeX

$$$\\text{rdropWhile p}(l ++ [x]) = \\text{rdropWhile p}(l)$, когда p x = true.$$

Lean4

@[simp]
theorem rdropWhile_concat_pos (x : α) (h : p x) : rdropWhile p (l ++ [x]) = rdropWhile p l := by
  rw [rdropWhile_concat, if_pos h]

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

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

Разделы

Аффилиация

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