rel_dropLast_getLast — Mathlib

English

If l is Pairwise R and a ∈ l.dropLast, then R(a, last(l)).

Русский

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

LaTeX

$$$(h : l.\\,Pairwise\\;R)\\ (ha : a \\in l.dropLast)\\Rightarrow R(a,\\ l.getLast).$$$

Lean4

theorem rel_dropLast_getLast (h : l.Pairwise R) (ha : a ∈ l.dropLast) :
    R a (l.getLast <| ne_nil_of_mem <| dropLast_subset _ ha) :=
  by
  rw [← pairwise_reverse] at h
  rw [getLast_eq_head_reverse]
  exact h.rel_head_tail (by rwa [tail_reverse, mem_reverse])

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