mem_rtakeWhile_imp

Mathlib.Data.List.DropRight

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

English

If x belongs to rtakeWhile p l, then p x holds.

Русский

Если x принадлежит rtakeWhile p l, то p x истинно.

LaTeX

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

Lean4

theorem mem_rtakeWhile_imp {x : α} (hx : x ∈ rtakeWhile p l) : p x :=
  by
  rw [rtakeWhile, mem_reverse] at hx
  exact mem_takeWhile_imp hx

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

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

Разделы

Аффилиация

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