ext_get_iff — Mathlib

English

Two lists are equal if and only if they have equal lengths and their corresponding elements are equal at every index.

Русский

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

LaTeX

$$$ l_1 = l_2 \iff \big( |l_1| = |l_2| \land \forall n, h_1, h_2,\; get\ l_1\langle n,h_1\rangle = get\ l_2\langle n,h_2\rangle \big) $$$

Lean4

theorem ext_get_iff {l₁ l₂ : List α} : l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩ :=
  by
  constructor
  · rintro rfl
    exact ⟨rfl, fun _ _ _ ↦ rfl⟩
  · intro ⟨h₁, h₂⟩
    exact ext_get h₁ h₂

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