English
If k = l, two functions f: Fin k → α and g: Fin l → α are HEq iff they agree after transporting indices along the equality.
Русский
Если k = l, две функции f: Fin k → α и g: Fin l → α эквивалентны в смысле HEq тогда и только тогда, когда они согласованы после переноса индексов через равенство.
LaTeX
$$$f \stackrel{HEq}{\sim} g \iff \forall i : Fin k,\ f i = g \langle i, h \rightharpoonup i.2\rangle$$$
Lean4
/-- Assume `k = l`. If two functions defined on `Fin k` and `Fin l` are equal on each element,
then they coincide (in the heq sense). -/
protected theorem heq_fun_iff {α : Sort*} {k l : ℕ} (h : k = l) {f : Fin k → α} {g : Fin l → α} :
f ≍ g ↔ ∀ i : Fin k, f i = g ⟨(i : ℕ), h ▸ i.2⟩ := by
subst h
simp [funext_iff]
