heq_ext_iff — Mathlib

English

Two Fin elements i and j are HEq iff their natural values coincide, given k=l.

Русский

Два элемента Fin равны по HEq тогда и только тогда, когда их натуральные значения совпадают, при условии k=l.

LaTeX

$$$i \stackrel{HEq}{\sim} j \iff i.\mathrm{val} = j.\mathrm{val}$$$

Lean4

/-- Two elements of `Fin k` and `Fin l` are heq iff their values in `ℕ` coincide. This requires
`k = l`. For the left implication without this assumption, see `val_eq_val_of_heq`. -/
protected theorem heq_ext_iff {k l : ℕ} (h : k = l) {i : Fin k} {j : Fin l} : i ≍ j ↔ (i : ℕ) = (j : ℕ) :=
  by
  subst h
  simp [val_eq_val]

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