mem_getLast?_cons — Mathlib

English

If x is in the last-option of a list, then x is in the last-option of any list with an added head element y.

Русский

Если x принадлежит getLast? l, то x принадлежит getLast? (y :: l).

LaTeX

$$$\forall {x}\ {l : List\, \alpha},\ x \in l.getLast? \Rightarrow x \in (y :: l).getLast?$$$

Lean4

theorem mem_getLast?_cons {x y : α} : ∀ {l : List α}, x ∈ l.getLast? → x ∈ (y :: l).getLast?
  | [], _ => by contradiction
  | _ :: _, h => h

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