head_some_of_get?_some — Mathlib

English

If some a ∈ get? s n, then there exists a' with some a' ∈ head s.

Русский

Если some a ∈ get?(s,n), то существует a' с some a' ∈ head s.

LaTeX

$$$$\text{some } a \in \mathrm{get?}(s,n) \Rightarrow \exists a'\, \text{some } a' \in \operatorname{head}(s).$$$$

Lean4

theorem head_some_of_get?_some {s : WSeq α} {a n} (h : some a ∈ get? s n) : ∃ a', some a' ∈ head s := by
  induction n generalizing a with
  | zero => exact ⟨_, h⟩
  | succ n IH =>
    let ⟨a', h'⟩ := head_some_of_head_tail_some h
    exact IH h'

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