val_eq_val_of_heq — Mathlib

English

If i ≍ j is a heterogeneous equality between Fin indices, then i.val = j.val.

Русский

Если i ≍ j — гетерогенная эквивалентность между индексами Fin, то i.val = j.val.

LaTeX

$$$\forall {k\ell}, \; {i : \mathrm{Fin}(k)}, {j : \mathrm{Fin}(\ell)}, (i \equiv\!\!\! j) \Rightarrow i.\mathrm{val} = j.\mathrm{val}$$$

Lean4

theorem val_eq_val_of_heq {k l : ℕ} {i : Fin k} {j : Fin l} (h : i ≍ j) : (i : ℕ) = (j : ℕ) :=
  (Fin.heq_ext_iff (fin_injective (type_eq_of_heq h))).1 h

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