rel_head_tail — Mathlib

English

If l is Pairwise R and a ∈ l.tail, then R(head(l), a).

Русский

Если l является Pairwise R и a ∈ хвост списка, то R(голова списка, a).

LaTeX

$$$(h_1 : l\\text{.Pairwise } R)\\ \\land\\ (ha : a \\in l.tail)\\ \\Rightarrow\\ R\\bigl(\\text{head}(l), a\\bigr).$$$

Lean4

theorem rel_head_tail (h₁ : l.Pairwise R) (ha : a ∈ l.tail) : R (l.head <| ne_nil_of_mem <| mem_of_mem_tail ha) a := by
  cases l with
  | nil => simp at ha
  | cons b l => exact (pairwise_cons.1 h₁).1 a ha

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