ext_getElem?_iff' — Mathlib

English

If two lists have equal lengths and their corresponding elements (via getElem!) are equal at every position, then the lists are equal.

Русский

Если два списка имеют равные длины и их элементы на каждом месте равны (по getElem!), то списки равны.

LaTeX

$$$ l_1.length = l_2.length \land \forall n,\; l_1[n]! = l_2[n]! \Rightarrow l_1 = l_2 $$$

Lean4

theorem ext_getElem?_iff' {l₁ l₂ : List α} : l₁ = l₂ ↔ ∀ n < max l₁.length l₂.length, l₁[n]? = l₂[n]? :=
  ⟨by rintro rfl _ _; rfl, ext_getElem?'⟩

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