mem_getLast?_append_of_mem_getLast?

English

For lists l1, l2 and element x, if x ∈ l2.getLast? then x ∈ (l1 ++ l2).getLast?.

Русский

Для списков l1, l2 и элемента x, если x ∈ l2.getLast?, то x ∈ (l1 ++ l2).getLast?.

LaTeX

$$$\\\\mathrm{Option.instMembership}.mem \\\\ (l_2.getLast?)\\\\ x \\\\Rightarrow \\\\mathrm{Option.instMembership}.mem \\\\ ((l_1 \\\\; ++ \\\\; l_2).getLast?) \\\\ x$$$

Lean4

theorem mem_getLast?_append_of_mem_getLast? {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.getLast?) : x ∈ (l₁ ++ l₂).getLast? :=
  by grind

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