ext_getElem! — Mathlib

English

If a family of element-wise equalities with GetElem! holds between two lists, then the lists are equal.

Русский

Если между двумя списками выполняются попарно равные значения через GetElem!, то списки равны.

LaTeX

$$$ (\forall n,\; \mathrm{getElem!}\ l_1\; n = \mathrm{getElem!}\ l_2\; n) \Rightarrow l_1 = l_2 $$$

Lean4

/-- If two lists `l₁` and `l₂` are the same length and `l₁[n]! = l₂[n]!` for all `n`,
then the lists are equal. -/
theorem ext_getElem! [Inhabited α] (hl : length l₁ = length l₂) (h : ∀ n : ℕ, l₁[n]! = l₂[n]!) : l₁ = l₂ :=
  ext_getElem hl fun n h₁ h₂ ↦ by simpa only [← getElem!_pos] using h n

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