rel_getLast — Mathlib

English

If R is IsRefl and l is Pairwise R, then for every a ∈ l, R(a, last(l)).

Русский

Если R рефлексивно и l является Pairwise R, то для любого a ∈ l, R(a, last(l)).

LaTeX

$$$[IsRefl\\;\\alpha\\;R] \\Rightarrow (h_1 : l.\\,Pairwise\\;R) \\Rightarrow (ha : a \\in l) \\Rightarrow R(a, l.getLast).$$$

Lean4

theorem rel_getLast [IsRefl α R] (h₁ : l.Pairwise R) (ha : a ∈ l) : R a (l.getLast <| ne_nil_of_mem ha) :=
  h₁.rel_getLast_of_rel_getLast_getLast ha (refl_of ..)

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