image_diag — Mathlib

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

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