ext_getElem?' — Mathlib

English

If for all n less than max(l1.length, l2.length) we have l1[n]? = l2[n]?, then l1 = l2.

Русский

Если для всех n меньше max(|l1|,|l2|) выполняется l1[n]? = l2[n]?, то списки равны.

LaTeX

$$$ (\forall n < \max(|l_1|,|l_2|),\; l_1[n]? = l_2[n]?) \Rightarrow l_1 = l_2 $$$

Lean4

theorem ext_getElem?' {l₁ l₂ : List α} (h' : ∀ n < max l₁.length l₂.length, l₁[n]? = l₂[n]?) : l₁ = l₂ :=
  by
  apply ext_getElem?
  grind

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