mem_getLast?_eq_getLast — Mathlib

English

If x is in the last optional of a list, then x is in the last optional of the list with an added head.

Русский

Если x принадлежит последнему элементу списка, то x принадлежит последнему элементу списка с добавленной головой.

LaTeX

$$$\forall {x}\ {l : List\, \alpha},\ Option.instMembership.mem l.getLast? x \Rightarrow Option.instMembership.mem (List.cons y l).getLast? x$$$

Lean4

theorem mem_getLast?_eq_getLast : ∀ {l : List α} {x : α}, x ∈ l.getLast? → ∃ h, x = getLast l h
  | [], x, hx | [a], x, hx | a :: b :: l, x, hx => by grind

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