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