Pairwise_cons_cons_head — Mathlib

English

If a relation R on α makes the 3-element sequence (hd, tl_hd, tl_tl) pairwise, then R(hd, tl_hd).

Русский

Если отношение R на множествах удовлетворяет попарному свойству для тройки hd, tl_hd, tl_tl, то выполнено R(hd, tl_hd).

LaTeX

$$$\\operatorname{Pairwise}(R, \\mathrm{cons}(hd, \\mathrm{cons}(tl\\_hd, tl\\_tl))) \\Rightarrow R(hd, tl\\_hd)$$$

Lean4

theorem Pairwise_cons_cons_head {R : α → α → Prop} {hd tl_hd : α} {tl_tl : Seq α}
    (h : Pairwise R (cons hd (cons tl_hd tl_tl))) : R hd tl_hd :=
  by
  simp only [Pairwise] at h
  simpa using h 0 1 Nat.one_pos

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