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