English
For any map f, the image of the diagonal of S under f equals the image of S under the map x ↦ f(x,x).
Русский
Образ диагонали S под отображением f равен образу S под отображением x ↦ f(x,x).
LaTeX
$$$\\mathrm{image}\ f\\ (s\\mathrm{.diag}) = \\mathrm{image}\\ (\\lambda x. f(x,x))\\ s$$$
Lean4
@[simp]
theorem image_diag [DecidableEq β] (f : α × α → β) (s : Finset α) : s.diag.image f = s.image fun x ↦ f (x, x) :=
by
ext y
aesop