applyId — Mathlib

English

Interpret a list of pairs as a total function by mapping each input to its paired output when present, otherwise leaving the input fixed.

Русский

Интерпретируем список пар как общую функцию: если вход совпадает с первой компонентой пары, возвращаем вторую компоненту; иначе возвращаем сам вход.

LaTeX

$$$\text{applyId}:[(a_i,b_i)](x) = \begin{cases} b_i & \text{если } x = a_i \text{ для некоторого } i, \\ x & \text{иначе}. \end{cases}$$$

Lean4

/-- Interpret a list of pairs as a total function, defaulting to
the identity function when no entries are found for a given function -/
def applyId [DecidableEq α] (xs : List (α × α)) (x : α) : α :=
  ((xs.map Prod.toSigma).dlookup x).getD x

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