head_some_of_head_tail_some — Mathlib

English

If some a ∈ head (tail s), then there exists a' with some a' ∈ head s.

Русский

Если some a входит в head(tail s), тогда существует a' с some a' ∈ head s.

LaTeX

$$$$\text{some } a \in \operatorname{head}(\operatorname{tail}(s)) \Rightarrow \exists a'\,\text{some } a' \in \operatorname{head}(s).$$$$

Lean4

theorem head_some_of_head_tail_some {s : WSeq α} {a} (h : some a ∈ head (tail s)) : ∃ a', some a' ∈ head s :=
  by
  unfold head at h
  rcases Computation.exists_of_mem_map h with ⟨o, md, e⟩; clear h
  rcases o with - | o <;> [injection e; injection e with h']; clear h'
  obtain ⟨a, am⟩ := destruct_some_of_destruct_tail_some md
  exact ⟨_, Computation.mem_map (@Prod.fst α (WSeq α) <$> ·) am⟩

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