mem_head?_append_of_mem_head? — Mathlib

English

If x ∈ head? s, then x ∈ (s ++ t).head?.

Русский

Если x является головой списка s, то x также присутствует как head? от s ++ t.

LaTeX

$$$\\\\mathrm{Option.instMembership}.mem \\\\ x \\\\ (s.head?) \\\\Rightarrow \\\\mathrm{Option.instMembership}.mem \\\\ x \\\\ ((s \\\\; ++ \\\\; t).head?)$$$

Lean4

theorem mem_head?_append_of_mem_head? {s t : List α} {x : α} (h : x ∈ s.head?) : x ∈ (s ++ t).head? := by
  grind [Option.mem_def]

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