get_length_sub_one — Mathlib

English

Two lists are equal if they have equal lengths and equal elements at every corresponding position when using the optional getElem values.

Русский

Два списка равны, если их длины равны и элементы на соответствующих позициях равны (с использованием опционального getElem).

LaTeX

$$$ l_1 = l_2 \iff \big( |l_1| = |l_2| \land \forall n,\; l_1[n]? = l_2[n]? \big) $$$

Lean4

theorem get_length_sub_one {l : List α} (h : l.length - 1 < l.length) :
    l.get ⟨l.length - 1, h⟩ = l.getLast (by rintro rfl; exact Nat.lt_irrefl 0 h) :=
  (getLast_eq_getElem _).symm

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