rel_getLast_of_rel_getLast_getLast

English

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

Русский

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

LaTeX

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

Lean4

theorem rel_getLast_of_rel_getLast_getLast (h₁ : l.Pairwise R) (ha : a ∈ l)
    (hlast : R (l.getLast <| ne_nil_of_mem ha) (l.getLast <| ne_nil_of_mem ha)) : R a (l.getLast <| ne_nil_of_mem ha) :=
  by
  rw [← dropLast_concat_getLast (ne_nil_of_mem ha), mem_append, List.mem_singleton] at ha
  exact ha.elim h₁.rel_dropLast_getLast (· ▸ hlast)

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