graph — Mathlib

English

The graph of a finitely supported function is the finite set of input-output pairs (a, f(a)) for a in the support.

Русский

График функции с конечной опорой — это конечное множество пар (a, f(a)) для a в опоре функции.

LaTeX

$$def\\ graph (f : α →₀ M) : Finset (α × M) := f.support.map (\\lambda a. (a, f a))$$

Lean4

/-- The graph of a finitely supported function over its support, i.e. the finset of input and output
pairs with non-zero outputs. -/
def graph (f : α →₀ M) : Finset (α × M) :=
  f.support.map ⟨fun a => Prod.mk a (f a), fun _ _ h => (Prod.mk.inj h).1⟩

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