rtakeWhile_nil

Mathlib.Data.List.DropRight

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

English

Taking from an empty list yields an empty list: rtakeWhile p [] = [].

Русский

Из пустого списка берется пустой: rtakeWhile p [] = [].

LaTeX

$$$$ \mathrm{rtakeWhile}(p, \emptyset) = \emptyset. $$$$

Lean4

@[simp]
theorem rtakeWhile_nil : rtakeWhile p ([] : List α) = [] := by simp [rtakeWhile]

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

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

Разделы

Аффилиация

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