rel_head_of_rel_head_head — Mathlib

English

If l is Pairwise with respect to R, a ∈ l, and R(head(l), head(l)) holds, then R(head(l), a).

Русский

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

LaTeX

$$$(h_1 : l\\text{.Pairwise } R)\\ (ha : a \\in l)\\ (hhead : R(\\text{head}(l), \\text{head}(l)))\\Rightarrow\\ R(\\text{head}(l), a).$$$

Lean4

theorem rel_head_of_rel_head_head (h₁ : l.Pairwise R) (ha : a ∈ l)
    (hhead : R (l.head <| ne_nil_of_mem ha) (l.head <| ne_nil_of_mem ha)) : R (l.head <| ne_nil_of_mem ha) a := by
  cases l with
  | nil => simp at ha
  | cons b l => exact (mem_cons.mp ha).elim (· ▸ hhead) ((pairwise_cons.1 h₁).1 _)

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