English
For a linear-ordered α and f: Fin n → α, the graph of f is the Finset of pairs (f(i), i) indexed by i ∈ Fin n, ordered lexicographically.
Русский
Для линейно упорядоченного множества α и функции f: Fin n → α граф функции f представляет собой конечное множество пар (f(i), i), индексируемых i ∈ Fin n, упорядованных лексикографически.
LaTeX
$$$\\mathrm{graph}(f) = \\mathrm{Finset.univ}.image(\\lambda i. (f(i), i)).$$$
Lean4
/-- `graph f` produces the finset of pairs `(f i, i)`
equipped with the lexicographic order.
-/
def graph (f : Fin n → α) : Finset (α ×ₗ Fin n) :=
Finset.univ.image fun i => (f i, i)
