edist_append_eq_max_edist — Mathlib

English

For finite m,n, and maps x,y : Fin m → α, Fin n → α, the edist of their concatenation equals the maximum of edists of each part.

Русский

Для конечных m,n и отображений x: Fin m → α, y: Fin n → α справедливо, что edist(Fin.append x y, Fin.append x2 y2) = max(edist x x2, edist y y2).

LaTeX

$$$\operatorname{edist}(\mathrm{append}(x,y),\mathrm{append}(x',y')) = \max(\operatorname{edist}(x,x'), \operatorname{edist}(y,y'))$$$

Lean4

theorem _root_.Fin.edist_append_eq_max_edist (m n : ℕ) {x x2 : Fin m → α} {y y2 : Fin n → α} :
    edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2) := by
  simp [edist_pi_def, Finset.sup_univ_eq_iSup, ← Equiv.iSup_comp (e := finSumFinEquiv), iSup_sum]

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